mathlib3 documentation

topology.metric_space.equicontinuity

Equicontinuity in metric spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.equicontinuous_at_iff_right {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {F : ι β α} {x₀ : β} :
equicontinuous_at F x₀ (ε : ), ε > 0 (∀ᶠ (x : β) in nhds x₀, (i : ι), has_dist.dist (F i x₀) (F i x) < ε)

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

theorem metric.equicontinuous_at_iff {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] {F : ι β α} {x₀ : β} :
equicontinuous_at F x₀ (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (x : β), has_dist.dist x x₀ < δ (i : ι), has_dist.dist (F i x₀) (F i x) < ε)

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

@[protected]
theorem metric.equicontinuous_at_iff_pair {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {F : ι β α} {x₀ : β} :
equicontinuous_at F x₀ (ε : ), ε > 0 ( (U : set β) (H : U nhds x₀), (x : β), x U (x' : β), x' U (i : ι), has_dist.dist (F i x) (F i x') < ε)

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

theorem metric.uniform_equicontinuous_iff_right {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [uniform_space β] {F : ι β α} :
uniform_equicontinuous F (ε : ), ε > 0 (∀ᶠ (xy : β × β) in uniformity β, (i : ι), has_dist.dist (F i xy.fst) (F i xy.snd) < ε)

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

theorem metric.uniform_equicontinuous_iff {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] {F : ι β α} :
uniform_equicontinuous F (ε : ), ε > 0 ( (δ : ) (H : δ > 0), (x y : β), has_dist.dist x y < δ (i : ι), has_dist.dist (F i x) (F i y) < ε)

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

theorem metric.equicontinuous_at_of_continuity_modulus {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [topological_space β] {x₀ : β} (b : β ) (b_lim : filter.tendsto b (nhds x₀) (nhds 0)) (F : ι β α) (H : ∀ᶠ (x : β) in nhds x₀, (i : ι), has_dist.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.uniform_equicontinuous_of_continuity_modulus {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] (b : ) (b_lim : filter.tendsto b (nhds 0) (nhds 0)) (F : ι β α) (H : (x y : β) (i : ι), has_dist.dist (F i x) (F i y) b (has_dist.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} [pseudo_metric_space α] {ι : Type u_3} [pseudo_metric_space β] (b : ) (b_lim : filter.tendsto b (nhds 0) (nhds 0)) (F : ι β α) (H : (x y : β) (i : ι), has_dist.dist (F i x) (F i y) b (has_dist.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.