Equicontinuity of a family of functions

Let X be a topological space and α a UniformSpace. 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

• EquicontinuousAt: equicontinuity of a family of functions at a point
• Equicontinuous: equicontinuity of a family of functions on the whole domain
• UniformEquicontinuous: 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 (↑) : ↥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.EquicontinuousAt, Set.Equicontinuous and Set.UniformEquicontinuous asserting the corresponding fact about the family (↑) : ↥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 EquicontinuousWithinAt or EquicontinuousOn), 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.

References

• [N. Bourbaki, General Topology, Chapter X][bourbaki1966]

Tags

equicontinuity, uniform convergence, ascoli

def EquicontinuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] (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

• EquicontinuousAt F x₀ = ∀ (U : Set (α × α)), U ∈ uniformity α → ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ U

@[inline, reducible]

abbrev Set.EquicontinuousAt {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] (H : Set (X → α)) (x₀ : X) : Prop

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

Equations

• Set.EquicontinuousAt H x₀ = EquicontinuousAt Subtype.val x₀

def Equicontinuous {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] (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

• Equicontinuous F = ∀ (x₀ : X), EquicontinuousAt F x₀

@[inline, reducible]

abbrev Set.Equicontinuous {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] (H : Set (X → α)) : Prop

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

Equations

• Set.Equicontinuous H = Equicontinuous Subtype.val

def UniformEquicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] (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

• UniformEquicontinuous F = ∀ (U : Set (α × α)), U ∈ uniformity α → ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ U

@[inline, reducible]

abbrev Set.UniformEquicontinuous {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] (H : Set (β → α)) : Prop

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

Equations

• Set.UniformEquicontinuous H = UniformEquicontinuous Subtype.val

Empty index type

@[simp]

theorem equicontinuousAt_empty {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [h : IsEmpty ι] (F : ι → X → α) (x₀ : X) : EquicontinuousAt F x₀

@[simp]

theorem equicontinuous_empty {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [IsEmpty ι] (F : ι → X → α) : Equicontinuous F

@[simp]

theorem uniformEquicontinuous_empty {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] [h : IsEmpty ι] (F : ι → β → α) : UniformEquicontinuous F

Finite index type

theorem equicontinuousAt_finite {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [Finite ι] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ∀ (i : ι), ContinuousAt (F i) x₀

theorem equicontinuous_finite {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [Finite ι] {F : ι → X → α} : Equicontinuous F ↔ ∀ (i : ι), Continuous (F i)

theorem uniformEquicontinuous_finite {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] [Finite ι] {F : ι → β → α} : UniformEquicontinuous F ↔ ∀ (i : ι), UniformContinuous (F i)

Index type with a unique element

theorem equicontinuousAt_unique {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [Unique ι] {F : ι → X → α} {x : X} : EquicontinuousAt F x ↔ ContinuousAt (F default) x

theorem equicontinuous_unique {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] [Unique ι] {F : ι → X → α} : Equicontinuous F ↔ Continuous (F default)

theorem uniformEquicontinuous_unique {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] [Unique ι] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (F default)

theorem equicontinuousAt_iff_pair {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ∀ (U : Set (α × α)), U ∈ uniformity α → ∃ V, 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 UniformEquicontinuous.equicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {F : ι → β → α} (h : UniformEquicontinuous F) : Equicontinuous F

Uniform equicontinuity implies equicontinuity.

theorem EquicontinuousAt.continuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (i : ι) : ContinuousAt (F i) x₀

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

theorem Set.EquicontinuousAt.continuousAt_of_mem {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {H : Set (X → α)} {x₀ : X} (h : Set.EquicontinuousAt H x₀) {f : X → α} (hf : f ∈ H) : ContinuousAt f x₀

theorem Equicontinuous.continuous {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} (h : Equicontinuous F) (i : ι) : Continuous (F i)

Each function of an equicontinuous family is continuous.

theorem Set.Equicontinuous.continuous_of_mem {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {H : Set (X → α)} (h : Set.Equicontinuous H) {f : X → α} (hf : f ∈ H) : Continuous f

theorem UniformEquicontinuous.uniformContinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {F : ι → β → α} (h : UniformEquicontinuous F) (i : ι) : UniformContinuous (F i)

Each function of a uniformly equicontinuous family is uniformly continuous.

theorem Set.UniformEquicontinuous.uniformContinuous_of_mem {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {H : Set (β → α)} (h : Set.UniformEquicontinuous H) {f : β → α} (hf : f ∈ H) : UniformContinuous f

theorem EquicontinuousAt.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (u : κ → ι) : EquicontinuousAt (F ∘ u) x₀

Taking sub-families preserves equicontinuity at a point.

theorem Set.EquicontinuousAt.mono {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {H : Set (X → α)} {H' : Set (X → α)} {x₀ : X} (h : Set.EquicontinuousAt H x₀) (hH : H' ⊆ H) : Set.EquicontinuousAt H' x₀

theorem Equicontinuous.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} (h : Equicontinuous F) (u : κ → ι) : Equicontinuous (F ∘ u)

Taking sub-families preserves equicontinuity.

theorem Set.Equicontinuous.mono {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {H : Set (X → α)} {H' : Set (X → α)} (h : Set.Equicontinuous H) (hH : H' ⊆ H) : Set.Equicontinuous H'

theorem UniformEquicontinuous.comp {ι : Type u_1} {κ : Type u_2} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {F : ι → β → α} (h : UniformEquicontinuous F) (u : κ → ι) : UniformEquicontinuous (F ∘ u)

Taking sub-families preserves uniform equicontinuity.

theorem Set.UniformEquicontinuous.mono {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {H : Set (β → α)} {H' : Set (β → α)} (h : Set.UniformEquicontinuous H) (hH : H' ⊆ H) : Set.UniformEquicontinuous H'

theorem equicontinuousAt_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀

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

theorem equicontinuous_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} : Equicontinuous F ↔ Equicontinuous Subtype.val

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

theorem uniformEquicontinuous_at_iff_range {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformEquicontinuous Subtype.val

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

theorem equicontinuousAt_iff_continuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} {x₀ : X} : EquicontinuousAt F x₀ ↔ ContinuousAt (↑UniformFun.ofFun ∘ Function.swap F) 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} [TopologicalSpace X] [UniformSpace α] {F : ι → X → α} : Equicontinuous F ↔ Continuous (↑UniformFun.ofFun ∘ Function.swap F)

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 uniformEquicontinuous_iff_uniformContinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (↑UniformFun.ofFun ∘ Function.swap 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 equicontinuousAt_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {α' : Type u_10} {u : κ → UniformSpace α'} {F : ι → X → α'} {x₀ : X} : EquicontinuousAt F x₀ ↔ ∀ (k : κ), EquicontinuousAt F x₀

theorem equicontinuous_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} [TopologicalSpace X] {α' : Type u_10} {u : κ → UniformSpace α'} {F : ι → X → α'} : Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

theorem uniformEquicontinuous_iInf_rng {ι : Type u_1} {κ : Type u_2} {β : Type u_7} [UniformSpace β] {α' : Type u_10} {u : κ → UniformSpace α'} {F : ι → β → α'} : UniformEquicontinuous F ↔ ∀ (k : κ), UniformEquicontinuous F

theorem equicontinuousAt_iInf_dom {ι : Type u_1} {κ : Type u_2} {α : Type u_6} [UniformSpace α] {X' : Type u_10} {t : κ → TopologicalSpace X'} {F : ι → X' → α} {x₀ : X'} {k : κ} (hk : EquicontinuousAt F x₀) : EquicontinuousAt F x₀

theorem equicontinuous_iInf_dom {ι : Type u_1} {κ : Type u_2} {α : Type u_6} [UniformSpace α] {X' : Type u_10} {t : κ → TopologicalSpace X'} {F : ι → X' → α} {k : κ} (hk : Equicontinuous F) : Equicontinuous F

theorem uniform_equicontinuous_infi_dom {ι : Type u_1} {κ : Type u_2} {α : Type u_6} [UniformSpace α] {β' : Type u_10} {u : κ → UniformSpace β'} {F : ι → β' → α} {k : κ} (hk : UniformEquicontinuous F) : UniformEquicontinuous F

theorem Filter.HasBasis.equicontinuousAt_iff_left {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {κ : Type u_10} {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {x₀ : X} (hX : Filter.HasBasis (nhds x₀) p s) : EquicontinuousAt F x₀ ↔ ∀ (U : Set (α × α)), U ∈ uniformity α → ∃ k, p k ∧ ∀ (x : X), x ∈ s k → ∀ (i : ι), (F i x₀, F i x) ∈ U

theorem Filter.HasBasis.equicontinuousAt_iff_right {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {κ : Type u_10} {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hα : Filter.HasBasis (uniformity α) p s) : EquicontinuousAt F x₀ ↔ ∀ (k : κ), p k → ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) ∈ s k

theorem Filter.HasBasis.equicontinuousAt_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {κ₁ : Type u_10} {κ₂ : Type u_11} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hX : Filter.HasBasis (nhds x₀) p₁ s₁) (hα : Filter.HasBasis (uniformity α) p₂ s₂) : EquicontinuousAt F x₀ ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x : X), x ∈ s₁ k₁ → ∀ (i : ι), (F i x₀, F i x) ∈ s₂ k₂

theorem Filter.HasBasis.uniformEquicontinuous_iff_left {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {κ : Type u_10} {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} (hβ : Filter.HasBasis (uniformity β) p s) : UniformEquicontinuous F ↔ ∀ (U : Set (α × α)), U ∈ uniformity α → ∃ k, p k ∧ ∀ (x y : β), (x, y) ∈ s k → ∀ (i : ι), (F i x, F i y) ∈ U

theorem Filter.HasBasis.uniformEquicontinuous_iff_right {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {κ : Type u_10} {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} (hα : Filter.HasBasis (uniformity α) p s) : UniformEquicontinuous F ↔ ∀ (k : κ), p k → ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), (F i xy.fst, F i xy.snd) ∈ s k

theorem Filter.HasBasis.uniformEquicontinuous_iff {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {κ₁ : Type u_10} {κ₂ : Type u_11} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α} (hβ : Filter.HasBasis (uniformity β) p₁ s₁) (hα : Filter.HasBasis (uniformity α) p₂ s₂) : UniformEquicontinuous F ↔ ∀ (k₂ : κ₂), p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ (x y : β), (x, y) ∈ s₁ k₁ → ∀ (i : ι), (F i x, F i y) ∈ s₂ k₂

theorem UniformInducing.equicontinuousAt_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] [UniformSpace α] [UniformSpace β] {F : ι → X → α} {x₀ : X} {u : α → β} (hu : UniformInducing u) : EquicontinuousAt F x₀ ↔ EquicontinuousAt ((fun x x_1 => x ∘ x_1) u ∘ F) 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 UniformInducing.equicontinuous_iff {ι : Type u_1} {X : Type u_3} {α : Type u_6} {β : Type u_7} [TopologicalSpace X] [UniformSpace α] [UniformSpace β] {F : ι → X → α} {u : α → β} (hu : UniformInducing u) : Equicontinuous F ↔ Equicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)

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 UniformInducing.uniformEquicontinuous_iff {ι : Type u_1} {α : Type u_6} {β : Type u_7} {γ : Type u_8} [UniformSpace α] [UniformSpace β] [UniformSpace γ] {F : ι → β → α} {u : α → γ} (hu : UniformInducing u) : UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x x_1 => x ∘ x_1) u ∘ F)

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 EquicontinuousAt.closure' {X : Type u_3} {Y : Type u_4} {α : Type u_6} [TopologicalSpace X] [TopologicalSpace Y] [UniformSpace α] {A : Set Y} {u : Y → X → α} {x₀ : X} (hA : EquicontinuousAt (u ∘ Subtype.val) x₀) (hu : Continuous u) : EquicontinuousAt (u ∘ Subtype.val) x₀

A version of EquicontinuousAt.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 FunLike types where the coercion is injective.

theorem EquicontinuousAt.closure {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {A : Set (X → α)} {x₀ : X} (hA : Set.EquicontinuousAt A x₀) : Set.EquicontinuousAt (closure A) 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.continuousAt_of_equicontinuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {l : Filter ι} [Filter.NeBot l] {F : ι → X → α} {f : X → α} {x₀ : X} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : EquicontinuousAt F x₀) : ContinuousAt f 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} [TopologicalSpace X] [TopologicalSpace Y] [UniformSpace α] {A : Set Y} {u : Y → X → α} (hA : Equicontinuous (u ∘ Subtype.val)) (hu : Continuous u) : Equicontinuous (u ∘ Subtype.val)

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 FunLike types where the coercion is injective.

theorem Equicontinuous.closure {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {A : Set (X → α)} (hA : Set.Equicontinuous A) : Set.Equicontinuous (closure A)

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

theorem Filter.Tendsto.continuous_of_equicontinuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {l : Filter ι} [Filter.NeBot l] {F : ι → X → α} {f : X → α} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : Equicontinuous F) : Continuous f

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

theorem UniformEquicontinuous.closure' {Y : Type u_4} {α : Type u_6} {β : Type u_7} [TopologicalSpace Y] [UniformSpace α] [UniformSpace β] {A : Set Y} {u : Y → β → α} (hA : UniformEquicontinuous (u ∘ Subtype.val)) (hu : Continuous u) : UniformEquicontinuous (u ∘ Subtype.val)

A version of UniformEquicontinuous.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 FunLike types where the coercion is injective.

theorem UniformEquicontinuous.closure {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {A : Set (β → α)} (hA : Set.UniformEquicontinuous A) : Set.UniformEquicontinuous (closure A)

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

theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {ι : Type u_1} {α : Type u_6} {β : Type u_7} [UniformSpace α] [UniformSpace β] {l : Filter ι} [Filter.NeBot l] {F : ι → β → α} {f : β → α} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : UniformEquicontinuous F) : UniformContinuous f

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

theorem EquicontinuousAt.tendsto_of_mem_closure {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {l : Filter ι} {F : ι → X → α} {f : X → α} {s : Set X} {x : X} {z : α} (hF : EquicontinuousAt F x) (hf : Filter.Tendsto f (nhdsWithin x s) (nhds z)) (hs : ∀ (y : X), y ∈ s → Filter.Tendsto (fun x => F x y) l (nhds (f y))) (hx : x ∈ closure s) : Filter.Tendsto (fun x => F x x) l (nhds z)

If F : ι → X → α is a family of functions equicontinuous at x, it tends to f y along a filter l for any y ∈ s, the limit function f tends to z along 𝓝[s] x, and x ∈ closure s, then (F · x) tends to z along l.

In some sense, this is a converse of EquicontinuousAt.closure.

theorem Equicontinuous.isClosed_setOf_tendsto {ι : Type u_1} {X : Type u_3} {α : Type u_6} [TopologicalSpace X] [UniformSpace α] {l : Filter ι} {F : ι → X → α} {f : X → α} (hF : Equicontinuous F) (hf : Continuous f) : IsClosed {x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}

If F : ι → X → α is an equicontinuous family of functions, f : X → α is a continuous function, and l is a filter on ι, then {x | Filter.Tendsto (F · x) l (𝓝 (f x))} is a closed set.