Documentation

Mathlib.Topology.MetricSpace.Equicontinuity

Equicontinuity in metric spaces #

This files contains various facts about (uniform) equicontinuity in metric spaces. Most importantly, we prove the usual characterization of equicontinuity of F at x₀ in the case of (pseudo) metric spaces: ∀ ε > 0, ∃ δ > 0, ∀ x, dist x x₀ < δ → ∀ i, dist (F i x₀) (F i x) < ε, and we prove that functions sharing a common (local or global) continuity modulus are (locally or uniformly) equicontinuous.

Main statements #

Tags #

equicontinuity, continuity modulus

theorem Metric.equicontinuousAt_iff_right {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {F : ιβα} {x₀ : β} :
EquicontinuousAt F x₀ ε > 0, ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Characterization of equicontinuity for families of functions taking values in a (pseudo) metric space.

theorem Metric.equicontinuousAt_iff {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] {F : ιβα} {x₀ : β} :
EquicontinuousAt F x₀ ε > 0, ∃ δ > 0, ∀ (x : β), dist x x₀ < δ∀ (i : ι), dist (F i x₀) (F i x) < ε

Characterization of equicontinuity for families of functions between (pseudo) metric spaces.

theorem Metric.equicontinuousAt_iff_pair {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {F : ιβα} {x₀ : β} :
EquicontinuousAt F x₀ ε > 0, ∃ U ∈ nhds x₀, xU, x'U, ∀ (i : ι), dist (F i x) (F i x') < ε

Reformulation of equicontinuousAt_iff_pair for families of functions taking values in a (pseudo) metric space.

theorem Metric.uniformEquicontinuous_iff_right {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [UniformSpace β] {F : ιβα} :
UniformEquicontinuous F ε > 0, ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), dist (F i xy.1) (F i xy.2) < ε

Characterization of uniform equicontinuity for families of functions taking values in a (pseudo) metric space.

theorem Metric.uniformEquicontinuous_iff {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] {F : ιβα} :
UniformEquicontinuous F ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ∀ (i : ι), dist (F i x) (F i y) < ε

Characterization of uniform equicontinuity for families of functions between (pseudo) metric spaces.

theorem Metric.equicontinuousAt_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [TopologicalSpace β] {x₀ : β} (b : β) (b_lim : Filter.Tendsto b (nhds x₀) (nhds 0)) (F : ιβα) (H : ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) b x) :

For a family of functions to a (pseudo) metric spaces, a convenient way to prove equicontinuity at a point is to show that all of the functions share a common local continuity modulus.

theorem Metric.uniformEquicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] (b : ) (b_lim : Filter.Tendsto b (nhds 0) (nhds 0)) (F : ιβα) (H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) b (dist x y)) :

For a family of functions between (pseudo) metric spaces, a convenient way to prove uniform equicontinuity is to show that all of the functions share a common global continuity modulus.

theorem Metric.equicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] {ι : Type u_4} [PseudoMetricSpace β] (b : ) (b_lim : Filter.Tendsto b (nhds 0) (nhds 0)) (F : ιβα) (H : ∀ (x y : β) (i : ι), dist (F i x) (F i y) b (dist x y)) :

For a family of functions between (pseudo) metric spaces, a convenient way to prove equicontinuity is to show that all of the functions share a common global continuity modulus.