# mathlib3documentation

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 #

• equicontinuous_at_iff: characterization of equicontinuity for families of functions between (pseudo) metric spaces.
• equicontinuous_at_of_continuity_modulus: convenient way to prove equicontinuity at a point of a family of functions to a (pseudo) metric space by showing that they share a common local continuity modulus.
• uniform_equicontinuous_of_continuity_modulus: convenient way to prove uniform equicontinuity of a family of functions to a (pseudo) metric space by showing that they share a common global continuity modulus.

## Tags #

equicontinuity, continuity modulus

theorem metric.equicontinuous_at_iff_right {α : Type u_1} {β : Type u_2} {ι : Type u_3} {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} {ι : Type u_3} {F : ι β α} {x₀ : β} :
(ε : ), ε > 0 ( (δ : ) (H : δ > 0), (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} {ι : Type u_3} {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} {ι : Type u_3} {F : ι β α} :
(ε : ), ε > 0 (∀ᶠ (xy : β × β) in , (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} {ι : Type u_3} {F : ι β α} :
(ε : ), ε > 0 ( (δ : ) (H : δ > 0), (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} {ι : Type u_3} {x₀ : β} (b : β ) (b_lim : (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} {ι : Type u_3} (b : ) (b_lim : (nhds 0) (nhds 0)) (F : ι β α) (H : (x y : β) (i : ι), has_dist.dist (F i x) (F i y) b 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} {ι : Type u_3} (b : ) (b_lim : (nhds 0) (nhds 0)) (F : ι β α) (H : (x y : β) (i : ι), has_dist.dist (F i x) (F i y) b 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.