# mathlib3documentation

topology.uniform_space.equicontinuity

# Equicontinuity of a family of functions #

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

Let X be a topological space and α a uniform_space. A family of functions F : ι → X → α is said to be equicontinuous at a point x₀ : X when, for any entourage U in α, there is a neighborhood V of x₀ such that, for all x ∈ V, and for all i, F i x is U-close to F i x₀. In other words, one has ∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ U. For maps between metric spaces, this corresponds to ∀ ε > 0, ∃ δ > 0, ∀ x, ∀ i, dist x₀ x < δ → dist (F i x₀) (F i x) < ε.

F is said to be equicontinuous if it is equicontinuous at each point.

A closely related concept is that of uniform equicontinuity of a family of functions F : ι → β → α between uniform spaces, which means that, for any entourage U in α, there is an entourage V in β such that, if x and y are V-close, then for all i, F i x and F i y are U-close. In other words, one has ∀ U ∈ 𝓤 α, ∀ᶠ xy in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ U. For maps between metric spaces, this corresponds to ∀ ε > 0, ∃ δ > 0, ∀ x y, ∀ i, dist x y < δ → dist (F i x₀) (F i x) < ε.

## Main definitions #

• equicontinuous_at: equicontinuity of a family of functions at a point
• equicontinuous: equicontinuity of a family of functions on the whole domain
• uniform_equicontinuous: uniform equicontinuity of a family of functions on the whole domain

## Main statements #

• equicontinuous_iff_continuous: equicontinuity can be expressed as a simple continuity condition between well-chosen function spaces. This is really useful for building up the theory.
• equicontinuous.closure: if a set of functions is equicontinuous, its closure for the topology of uniform convergence is also equicontinuous.

## Notations #

Throughout this file, we use :

• ι, κ for indexing types
• X, Y, Z for topological spaces
• α, β, γ for uniform spaces

## Implementation details #

We choose to express equicontinuity as a properties of indexed families of functions rather than sets of functions for the following reasons:

• it is really easy to express equicontinuity of H : set (X → α) using our setup: it is just equicontinuity of the family coe : ↥H → (X → α). On the other hand, going the other way around would require working with the range of the family, which is always annoying because it introduces useless existentials.
• in most applications, one doesn't work with bare functions but with a more specific hom type hom. Equicontinuity of a set H : set hom would then have to be expressed as equicontinuity of coe_fn '' H, which is super annoying to work with. This is much simpler with families, because equicontinuity of a family 𝓕 : ι → hom would simply be expressed as equicontinuity of coe_fn ∘ 𝓕, which doesn't introduce any nasty existentials.

To simplify statements, we do provide abbreviations set.equicontinuous_at, set.equicontinuous and set.uniform_equicontinuous asserting the corresponding fact about the family coe : ↥H → (X → α) where H : set (X → α). Note however that these won't work for sets of hom types, and in that case one should go back to the family definition rather than using set.image.

Since we have no use case for it yet, we don't introduce any relative version (i.e no equicontinuous_within_at or equicontinuous_on), but this is more of a conservative position than a design decision, so anyone needing relative versions should feel free to add them, and that should hopefully be a straightforward task.

## Tags #

equicontinuity, uniform convergence, ascoli

def equicontinuous_at {ι : Type u_1} {X : Type u_3} {α : Type u_6} (F : ι X α) (x₀ : X) :
Prop

A family F : ι → X → α of functions from a topological space to a uniform space is equicontinuous at x₀ : X if, for all entourage U ∈ 𝓤 α, there is a neighborhood V of x₀ such that, for all x ∈ V and for all i : ι, F i x is U-close to F i x₀.

Equations
@[protected, reducible]
def set.equicontinuous_at {X : Type u_3} {α : Type u_6} (H : set (X α)) (x₀ : X) :
Prop

We say that a set H : set (X → α) of functions is equicontinuous at a point if the family coe : ↥H → (X → α) is equicontinuous at that point.

def equicontinuous {ι : Type u_1} {X : Type u_3} {α : Type u_6} (F : ι X α) :
Prop

A family F : ι → X → α of functions from a topological space to a uniform space is equicontinuous on all of X if it is equicontinuous at each point of X.

Equations
@[protected, reducible]
def set.equicontinuous {X : Type u_3} {α : Type u_6} (H : set (X α)) :
Prop

We say that a set H : set (X → α) of functions is equicontinuous if the family coe : ↥H → (X → α) is equicontinuous.

def uniform_equicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} (F : ι β α) :
Prop

A family F : ι → β → α of functions between uniform spaces is uniformly equicontinuous if, for all entourage U ∈ 𝓤 α, there is an entourage V ∈ 𝓤 β such that, whenever x and y are V-close, we have that, for all i : ι, F i x is U-close to F i x₀.

Equations
@[protected, reducible]
def set.uniform_equicontinuous {α : Type u_6} {β : Type u_7} (H : set α)) :
Prop

We say that a set H : set (X → α) of functions is uniformly equicontinuous if the family coe : ↥H → (X → α) is uniformly equicontinuous.

theorem equicontinuous_at_iff_pair {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} {x₀ : X} :
(U : set × α)), U ( (V : set X) (H : V nhds x₀), (x : X), x V (y : X), y V (i : ι), (F i x, F i y) U)

Reformulation of equicontinuity at x₀ comparing two variables near x₀ instead of comparing only one with x₀.

theorem uniform_equicontinuous.equicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} {F : ι β α} (h : uniform_equicontinuous F) :

Uniform equicontinuity implies equicontinuity.

theorem equicontinuous_at.continuous_at {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} {x₀ : X} (h : x₀) (i : ι) :
continuous_at (F i) x₀

Each function of a family equicontinuous at x₀ is continuous at x₀.

@[protected]
theorem set.equicontinuous_at.continuous_at_of_mem {X : Type u_3} {α : Type u_6} {H : set (X α)} {x₀ : X} (h : H.equicontinuous_at x₀) {f : X α} (hf : f H) :
x₀
theorem equicontinuous.continuous {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} (h : equicontinuous F) (i : ι) :

Each function of an equicontinuous family is continuous.

@[protected]
theorem set.equicontinuous.continuous_of_mem {X : Type u_3} {α : Type u_6} {H : set (X α)} (h : H.equicontinuous) {f : X α} (hf : f H) :
theorem uniform_equicontinuous.uniform_continuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} {F : ι β α} (h : uniform_equicontinuous F) (i : ι) :

Each function of a uniformly equicontinuous family is uniformly continuous.

@[protected]
theorem set.uniform_equicontinuous.uniform_continuous_of_mem {α : Type u_6} {β : Type u_7} {H : set α)} (h : H.uniform_equicontinuous) {f : β α} (hf : f H) :
theorem equicontinuous_at.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} {F : ι X α} {x₀ : X} (h : x₀) (u : κ ι) :

Taking sub-families preserves equicontinuity at a point.

@[protected]
theorem set.equicontinuous_at.mono {X : Type u_3} {α : Type u_6} {H H' : set (X α)} {x₀ : X} (h : H.equicontinuous_at x₀) (hH : H' H) :
theorem equicontinuous.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} {F : ι X α} (h : equicontinuous F) (u : κ ι) :

Taking sub-families preserves equicontinuity.

@[protected]
theorem set.equicontinuous.mono {X : Type u_3} {α : Type u_6} {H H' : set (X α)} (h : H.equicontinuous) (hH : H' H) :
theorem uniform_equicontinuous.comp {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_7} {F : ι β α} (h : uniform_equicontinuous F) (u : κ ι) :

Taking sub-families preserves uniform equicontinuity.

@[protected]
theorem set.uniform_equicontinuous.mono {α : Type u_6} {β : Type u_7} {H H' : set α)} (h : H.uniform_equicontinuous) (hH : H' H) :
theorem equicontinuous_at_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} {x₀ : X} :

A family 𝓕 : ι → X → α is equicontinuous at x₀ iff range 𝓕 is equicontinuous at x₀, i.e the family coe : range F → X → α is equicontinuous at x₀.

theorem equicontinuous_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} :

A family 𝓕 : ι → X → α is equicontinuous iff range 𝓕 is equicontinuous, i.e the family coe : range F → X → α is equicontinuous.

theorem uniform_equicontinuous_at_iff_range {ι : Type u_1} {α : Type u_6} {β : Type u_7} {F : ι β α} :

A family 𝓕 : ι → β → α is uniformly equicontinuous iff range 𝓕 is uniformly equicontinuous, i.e the family coe : range F → β → α is uniformly equicontinuous.

theorem equicontinuous_at_iff_continuous_at {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} {x₀ : X} :

A family 𝓕 : ι → X → α is equicontinuous at x₀ iff the function swap 𝓕 : X → ι → α is continuous at x₀ when ι → α is equipped with the topology of uniform convergence. This is very useful for developping the equicontinuity API, but it should not be used directly for other purposes.

theorem equicontinuous_iff_continuous {ι : Type u_1} {X : Type u_3} {α : Type u_6} {F : ι X α} :

A family 𝓕 : ι → X → α is equicontinuous iff the function swap 𝓕 : X → ι → α is continuous when ι → α is equipped with the topology of uniform convergence. This is very useful for developping the equicontinuity API, but it should not be used directly for other purposes.

theorem uniform_equicontinuous_iff_uniform_continuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} {F : ι β α} :

A family 𝓕 : ι → β → α is uniformly equicontinuous iff the function swap 𝓕 : β → ι → α is uniformly continuous when ι → α is equipped with the uniform structure of uniform convergence. This is very useful for developping the equicontinuity API, but it should not be used directly for other purposes.

theorem filter.has_basis.equicontinuous_at_iff_left {ι : Type u_1} {X : Type u_3} {α : Type u_6} {κ : Type u_2} {p : κ Prop} {s : κ set X} {F : ι X α} {x₀ : X} (hX : (nhds x₀).has_basis p s) :
(U : set × α)), U ( (k : κ) (_x : p k), (x : X), x s k (i : ι), (F i x₀, F i x) U)
theorem filter.has_basis.equicontinuous_at_iff_right {ι : Type u_1} {X : Type u_3} {α : Type u_6} {κ : Type u_2} {p : κ Prop} {s : κ set × α)} {F : ι X α} {x₀ : X} (hα : (uniformity α).has_basis p s) :
(k : κ), p k (∀ᶠ (x : X) in nhds x₀, (i : ι), (F i x₀, F i x) s k)
theorem filter.has_basis.equicontinuous_at_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} {κ₁ : Type u_2} {κ₂ : Type u_4} {p₁ : κ₁ Prop} {s₁ : κ₁ set X} {p₂ : κ₂ Prop} {s₂ : κ₂ set × α)} {F : ι X α} {x₀ : X} (hX : (nhds x₀).has_basis p₁ s₁) (hα : (uniformity α).has_basis p₂ s₂) :
(k₂ : κ₂), p₂ k₂ ( (k₁ : κ₁) (_x : p₁ k₁), (x : X), x s₁ k₁ (i : ι), (F i x₀, F i x) s₂ k₂)
theorem filter.has_basis.uniform_equicontinuous_iff_left {ι : Type u_1} {α : Type u_6} {β : Type u_7} {κ : Type u_2} {p : κ Prop} {s : κ set × β)} {F : ι β α} (hβ : (uniformity β).has_basis p s) :
(U : set × α)), U ( (k : κ) (_x : p k), (x y : β), (x, y) s k (i : ι), (F i x, F i y) U)
theorem filter.has_basis.uniform_equicontinuous_iff_right {ι : Type u_1} {α : Type u_6} {β : Type u_7} {κ : Type u_2} {p : κ Prop} {s : κ set × α)} {F : ι β α} (hα : (uniformity α).has_basis p s) :
(k : κ), p k (∀ᶠ (xy : β × β) in , (i : ι), (F i xy.fst, F i xy.snd) s k)
theorem filter.has_basis.uniform_equicontinuous_iff {ι : Type u_1} {α : Type u_6} {β : Type u_7} {κ₁ : Type u_2} {κ₂ : Type u_3} {p₁ : κ₁ Prop} {s₁ : κ₁ set × β)} {p₂ : κ₂ Prop} {s₂ : κ₂ set × α)} {F : ι β α} (hβ : (uniformity β).has_basis p₁ s₁) (hα : (uniformity α).has_basis p₂ s₂) :
(k₂ : κ₂), p₂ k₂ ( (k₁ : κ₁) (_x : p₁ k₁), (x y : β), (x, y) s₁ k₁ (i : ι), (F i x, F i y) s₂ k₂)
theorem uniform_inducing.equicontinuous_at_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_7} {F : ι X α} {x₀ : X} {u : α β} (hu : uniform_inducing u) :
x₀

Given u : α → β a uniform inducing map, a family 𝓕 : ι → X → α is equicontinuous at a point x₀ : X iff the family 𝓕', obtained by precomposing each function of 𝓕 by u, is equicontinuous at x₀.

theorem uniform_inducing.equicontinuous_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_7} {F : ι X α} {u : α β} (hu : uniform_inducing u) :

Given u : α → β a uniform inducing map, a family 𝓕 : ι → X → α is equicontinuous iff the family 𝓕', obtained by precomposing each function of 𝓕 by u, is equicontinuous.

theorem uniform_inducing.uniform_equicontinuous_iff {ι : Type u_1} {α : Type u_6} {β : Type u_7} {γ : Type u_8} {F : ι β α} {u : α γ} (hu : uniform_inducing u) :

Given u : α → γ a uniform inducing map, a family 𝓕 : ι → β → α is uniformly equicontinuous iff the family 𝓕', obtained by precomposing each function of 𝓕 by u, is uniformly equicontinuous.

theorem equicontinuous_at.closure' {X : Type u_3} {Y : Type u_4} {α : Type u_6} {A : set Y} {u : Y X α} {x₀ : X} (hA : x₀) (hu : continuous u) :
x₀

A version of equicontinuous_at.closure applicable to subsets of types which embed continuously into X → α with the product topology. It turns out we don't need any other condition on the embedding than continuity, but in practice this will mostly be applied to fun_like types where the coercion is injective.

theorem equicontinuous_at.closure {X : Type u_3} {α : Type u_6} {A : set (X α)} {x₀ : X} (hA : A.equicontinuous_at x₀) :
x₀

If a set of functions is equicontinuous at some x₀, its closure for the product topology is also equicontinuous at x₀.

theorem filter.tendsto.continuous_at_of_equicontinuous_at {ι : Type u_1} {X : Type u_3} {α : Type u_6} {l : filter ι} [l.ne_bot] {F : ι X α} {f : X α} {x₀ : X} (h₁ : (nhds f)) (h₂ : x₀) :
x₀

If 𝓕 : ι → X → α tends to f : X → α pointwise along some nontrivial filter, and if the family 𝓕 is equicontinuous at some x₀ : X, then the limit is continuous at x₀.

theorem equicontinuous.closure' {X : Type u_3} {Y : Type u_4} {α : Type u_6} {A : set Y} {u : Y X α} (hA : equicontinuous (u coe)) (hu : continuous u) :

A version of equicontinuous.closure applicable to subsets of types which embed continuously into X → α with the product topology. It turns out we don't need any other condition on the embedding than continuity, but in practice this will mostly be applied to fun_like types where the coercion is injective.

theorem equicontinuous.closure {X : Type u_3} {α : Type u_6} {A : set (X α)} (hA : A.equicontinuous) :

If a set of functions is equicontinuous, its closure for the product topology is also equicontinuous.

theorem filter.tendsto.continuous_of_equicontinuous_at {ι : Type u_1} {X : Type u_3} {α : Type u_6} {l : filter ι} [l.ne_bot] {F : ι X α} {f : X α} (h₁ : (nhds f)) (h₂ : equicontinuous F) :

If 𝓕 : ι → X → α tends to f : X → α pointwise along some nontrivial filter, and if the family 𝓕 is equicontinuous, then the limit is continuous.

theorem uniform_equicontinuous.closure' {Y : Type u_4} {α : Type u_6} {β : Type u_7} {A : set Y} {u : Y β α} (hA : uniform_equicontinuous (u coe)) (hu : continuous u) :

A version of uniform_equicontinuous.closure applicable to subsets of types which embed continuously into β → α with the product topology. It turns out we don't need any other condition on the embedding than continuity, but in practice this will mostly be applied to fun_like types where the coercion is injective.

theorem uniform_equicontinuous.closure {α : Type u_6} {β : Type u_7} {A : set α)} (hA : A.uniform_equicontinuous) :

If a set of functions is uniformly equicontinuous, its closure for the product topology is also uniformly equicontinuous.

theorem filter.tendsto.uniform_continuous_of_uniform_equicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} {l : filter ι} [l.ne_bot] {F : ι β α} {f : β α} (h₁ : (nhds f)) (h₂ : uniform_equicontinuous F) :

If 𝓕 : ι → β → α tends to f : β → α pointwise along some nontrivial filter, and if the family 𝓕 is uniformly equicontinuous, then the limit is uniformly continuous.