# 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

We also introduce relative versions, namely EquicontinuousWithinAt, EquicontinuousOn and UniformEquicontinuousOn, akin to ContinuousWithinAt, ContinuousOn and UniformContinuousOn respectively.

## 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 pointwise 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.

## References #

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

## Tags #

equicontinuity, uniform convergence, ascoli

def EquicontinuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) (x₀ : X) :

A family F : ι → X → α of functions from a topological space to a uniform space is equicontinuous at x₀ : X if, for all entourages 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
• = U ∈ , ∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) U
Instances For
@[reducible, inline]
abbrev Set.EquicontinuousAt {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (H : Set (Xα)) (x₀ : X) :

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
Instances For
def EquicontinuousWithinAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) (S : Set X) (x₀ : X) :

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

Equations
• = U ∈ , ∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) U
Instances For
@[reducible, inline]
abbrev Set.EquicontinuousWithinAt {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (H : Set (Xα)) (S : Set X) (x₀ : X) :

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

Equations
Instances For
def Equicontinuous {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) :

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
• = ∀ (x₀ : X),
Instances For
@[reducible, inline]
abbrev Set.Equicontinuous {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (H : Set (Xα)) :

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

Equations
Instances For
def EquicontinuousOn {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) (S : Set X) :

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

Equations
• = x₀S,
Instances For
@[reducible, inline]
abbrev Set.EquicontinuousOn {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (H : Set (Xα)) (S : Set X) :

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

Equations
Instances For
def UniformEquicontinuous {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (F : ιβα) :

A family F : ι → β → α of functions between uniform spaces is uniformly equicontinuous if, for all entourages 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 y.

Equations
• = U ∈ , ∀ᶠ (xy : β × β) in , ∀ (i : ι), (F i xy.1, F i xy.2) U
Instances For
@[reducible, inline]
abbrev Set.UniformEquicontinuous {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (H : Set (βα)) :

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

Equations
Instances For
def UniformEquicontinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (F : ιβα) (S : Set β) :

A family F : ι → β → α of functions between uniform spaces is uniformly equicontinuous on S : Set β if, for all entourages U ∈ 𝓤 α, there is a relative entourage V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S) such that, whenever x and y are V-close, we have that, for all i : ι, F i x is U-close to F i y.

Equations
Instances For
@[reducible, inline]
abbrev Set.UniformEquicontinuousOn {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (H : Set (βα)) (S : Set β) :

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

Equations
Instances For
theorem EquicontinuousAt.equicontinuousWithinAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} (H : ) (S : Set X) :
theorem EquicontinuousWithinAt.mono {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} {S : Set X} {T : Set X} (H : ) (hST : S T) :
@[simp]
theorem equicontinuousWithinAt_univ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) (x₀ : X) :
EquicontinuousWithinAt F Set.univ x₀
theorem equicontinuousAt_restrict_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) {S : Set X} (x₀ : S) :
EquicontinuousAt (S.restrict F) x₀
theorem Equicontinuous.equicontinuousOn {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} (H : ) (S : Set X) :
theorem EquicontinuousOn.mono {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {T : Set X} (H : ) (hST : S T) :
theorem equicontinuousOn_univ {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) :
EquicontinuousOn F Set.univ
theorem equicontinuous_restrict_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] (F : ιXα) {S : Set X} :
Equicontinuous (S.restrict F)
theorem UniformEquicontinuous.uniformEquicontinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} (H : ) (S : Set β) :
theorem UniformEquicontinuousOn.mono {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} {T : Set β} (H : ) (hST : S T) :
theorem uniformEquicontinuousOn_univ {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (F : ιβα) :
theorem uniformEquicontinuous_restrict_iff {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] (F : ιβα) {S : Set β} :
UniformEquicontinuous (S.restrict F)

### Empty index type #

@[simp]
theorem equicontinuousAt_empty {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [h : ] (F : ιXα) (x₀ : X) :
@[simp]
theorem equicontinuousWithinAt_empty {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [h : ] (F : ιXα) (S : Set X) (x₀ : X) :
@[simp]
theorem equicontinuous_empty {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] (F : ιXα) :
@[simp]
theorem equicontinuousOn_empty {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] (F : ιXα) (S : Set X) :
@[simp]
theorem uniformEquicontinuous_empty {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [h : ] (F : ιβα) :
@[simp]
theorem uniformEquicontinuousOn_empty {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [h : ] (F : ιβα) (S : Set β) :

### Finite index type #

theorem equicontinuousAt_finite {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {x₀ : X} :
∀ (i : ι), ContinuousAt (F i) x₀
theorem equicontinuousWithinAt_finite {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {S : Set X} {x₀ : X} :
∀ (i : ι), ContinuousWithinAt (F i) S x₀
theorem equicontinuous_finite {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} :
∀ (i : ι), Continuous (F i)
theorem equicontinuousOn_finite {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {S : Set X} :
∀ (i : ι), ContinuousOn (F i) S
theorem uniformEquicontinuous_finite {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [] {F : ιβα} :
∀ (i : ι), UniformContinuous (F i)
theorem uniformEquicontinuousOn_finite {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [] {F : ιβα} {S : Set β} :
∀ (i : ι), UniformContinuousOn (F i) S

### Index type with a unique element #

theorem equicontinuousAt_unique {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {x : X} :
ContinuousAt (F default) x
theorem equicontinuousWithinAt_unique {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {S : Set X} {x : X} :
ContinuousWithinAt (F default) S x
theorem equicontinuous_unique {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} :
Continuous (F default)
theorem equicontinuousOn_unique {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] [] {F : ιXα} {S : Set X} :
ContinuousOn (F default) S
theorem uniformEquicontinuous_unique {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [] {F : ιβα} :
UniformContinuous (F default)
theorem uniformEquicontinuousOn_unique {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] [] {F : ιβα} {S : Set β} :
UniformContinuousOn (F default) S
theorem equicontinuousWithinAt_iff_pair {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {x₀ : X} (hx₀ : x₀ S) :
U, VnhdsWithin x₀ S, xV, yV, ∀ (i : ι), (F i x, F i y) U

Reformulation of equicontinuity at x₀ within a set S, comparing two variables near x₀ instead of comparing only one with x₀.

theorem equicontinuousAt_iff_pair {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} :
U, Vnhds x₀, xV, yV, ∀ (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_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} (h : ) :

Uniform equicontinuity implies equicontinuity.

theorem UniformEquicontinuousOn.equicontinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} (h : ) :

Uniform equicontinuity on a subset implies equicontinuity on that subset.

theorem EquicontinuousAt.continuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} (h : ) (i : ι) :
ContinuousAt (F i) x₀

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

theorem EquicontinuousWithinAt.continuousWithinAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {x₀ : X} (h : ) (i : ι) :
ContinuousWithinAt (F i) S x₀

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

theorem Set.EquicontinuousAt.continuousAt_of_mem {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {x₀ : X} (h : H.EquicontinuousAt x₀) {f : Xα} (hf : f H) :
theorem Set.EquicontinuousWithinAt.continuousWithinAt_of_mem {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) {f : Xα} (hf : f H) :
theorem Equicontinuous.continuous {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} (h : ) (i : ι) :

Each function of an equicontinuous family is continuous.

theorem EquicontinuousOn.continuousOn {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} (h : ) (i : ι) :
ContinuousOn (F i) S

Each function of a family equicontinuous on S is continuous on S.

theorem Set.Equicontinuous.continuous_of_mem {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} (h : H.Equicontinuous) {f : Xα} (hf : f H) :
theorem Set.EquicontinuousOn.continuousOn_of_mem {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {S : Set X} (h : H.EquicontinuousOn S) {f : Xα} (hf : f H) :
theorem UniformEquicontinuous.uniformContinuous {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} (h : ) (i : ι) :

Each function of a uniformly equicontinuous family is uniformly continuous.

theorem UniformEquicontinuousOn.uniformContinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} (h : ) (i : ι) :

Each function of a family uniformly equicontinuous on S is uniformly continuous on S.

theorem Set.UniformEquicontinuous.uniformContinuous_of_mem {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {H : Set (βα)} (h : H.UniformEquicontinuous) {f : βα} (hf : f H) :
theorem Set.UniformEquicontinuousOn.uniformContinuousOn_of_mem {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {H : Set (βα)} {S : Set β} (h : H.UniformEquicontinuousOn S) {f : βα} (hf : f H) :
theorem EquicontinuousAt.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} (h : ) (u : κι) :

Taking sub-families preserves equicontinuity at a point.

theorem EquicontinuousWithinAt.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {x₀ : X} (h : ) (u : κι) :

Taking sub-families preserves equicontinuity at a point within a subset.

theorem Set.EquicontinuousAt.mono {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {H' : Set (Xα)} {x₀ : X} (h : H.EquicontinuousAt x₀) (hH : H' H) :
H'.EquicontinuousAt x₀
theorem Set.EquicontinuousWithinAt.mono {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {H' : Set (Xα)} {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) (hH : H' H) :
H'.EquicontinuousWithinAt S x₀
theorem Equicontinuous.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} (h : ) (u : κι) :

Taking sub-families preserves equicontinuity.

theorem EquicontinuousOn.comp {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} (h : ) (u : κι) :

Taking sub-families preserves equicontinuity on a subset.

theorem Set.Equicontinuous.mono {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {H' : Set (Xα)} (h : H.Equicontinuous) (hH : H' H) :
H'.Equicontinuous
theorem Set.EquicontinuousOn.mono {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {H : Set (Xα)} {H' : Set (Xα)} {S : Set X} (h : H.EquicontinuousOn S) (hH : H' H) :
H'.EquicontinuousOn S
theorem UniformEquicontinuous.comp {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} (h : ) (u : κι) :

Taking sub-families preserves uniform equicontinuity.

theorem UniformEquicontinuousOn.comp {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} (h : ) (u : κι) :

Taking sub-families preserves uniform equicontinuity on a subset.

theorem Set.UniformEquicontinuous.mono {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {H : Set (βα)} {H' : Set (βα)} (h : H.UniformEquicontinuous) (hH : H' H) :
H'.UniformEquicontinuous
theorem Set.UniformEquicontinuousOn.mono {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {H : Set (βα)} {H' : Set (βα)} {S : Set β} (h : H.UniformEquicontinuousOn S) (hH : H' H) :
H'.UniformEquicontinuousOn S
theorem equicontinuousAt_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : 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 equicontinuousWithinAt_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {x₀ : X} :
EquicontinuousWithinAt Subtype.val S x₀

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

theorem equicontinuous_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} :
Equicontinuous Subtype.val

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

theorem equicontinuousOn_iff_range {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} :
EquicontinuousOn Subtype.val S

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

theorem uniformEquicontinuous_iff_range {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} :

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

theorem uniformEquicontinuousOn_iff_range {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} :

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

theorem equicontinuousAt_iff_continuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {x₀ : X} :
ContinuousAt (UniformFun.ofFun ) 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 equicontinuousWithinAt_iff_continuousWithinAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} {x₀ : X} :
ContinuousWithinAt (UniformFun.ofFun ) S x₀

A family 𝓕 : ι → X → α is equicontinuous at x₀ within S iff the function swap 𝓕 : X → ι → α is continuous at x₀ within S 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_7} [tX : ] [uα : ] {F : ιXα} :
Continuous (UniformFun.ofFun )

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 equicontinuousOn_iff_continuousOn {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {F : ιXα} {S : Set X} :
ContinuousOn (UniformFun.ofFun ) S

A family 𝓕 : ι → X → α is equicontinuous on S iff the function swap 𝓕 : X → ι → α is continuous on S 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_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} :
UniformContinuous (UniformFun.ofFun )

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 uniformEquicontinuousOn_iff_uniformContinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {F : ιβα} {S : Set β} :
UniformContinuousOn (UniformFun.ofFun ) S

A family 𝓕 : ι → β → α is uniformly equicontinuous on S iff the function swap 𝓕 : β → ι → α is uniformly continuous on S 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 equicontinuousWithinAt_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_8} [tX : ] {u : κ} {F : ιXα'} {S : Set X} {x₀ : X} :
∀ (k : κ),
theorem equicontinuousAt_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_8} [tX : ] {u : κ} {F : ιXα'} {x₀ : X} :
∀ (k : κ),
theorem equicontinuous_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_8} [tX : ] {u : κ} {F : ιXα'} :
∀ (k : κ),
theorem equicontinuousOn_iInf_rng {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α' : Type u_8} [tX : ] {u : κ} {F : ιXα'} {S : Set X} :
∀ (k : κ),
theorem uniformEquicontinuous_iInf_rng {ι : Type u_1} {κ : Type u_2} {α' : Type u_8} {β : Type u_9} [uβ : ] {u : κ} {F : ιβα'} :
∀ (k : κ),
theorem uniformEquicontinuousOn_iInf_rng {ι : Type u_1} {κ : Type u_2} {α' : Type u_8} {β : Type u_9} [uβ : ] {u : κ} {F : ιβα'} {S : Set β} :
∀ (k : κ),
theorem equicontinuousWithinAt_iInf_dom {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_7} [uα : ] {t : κ} {F : ιX'α} {S : Set X'} {x₀ : X'} {k : κ} (hk : ) :
theorem equicontinuousAt_iInf_dom {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_7} [uα : ] {t : κ} {F : ιX'α} {x₀ : X'} {k : κ} (hk : ) :
theorem equicontinuous_iInf_dom {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_7} [uα : ] {t : κ} {F : ιX'α} {k : κ} (hk : ) :
theorem equicontinuousOn_iInf_dom {ι : Type u_1} {κ : Type u_2} {X' : Type u_4} {α : Type u_7} [uα : ] {t : κ} {F : ιX'α} {S : Set X'} {k : κ} (hk : ) :
theorem uniformEquicontinuous_iInf_dom {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β' : Type u_10} [uα : ] {u : κ} {F : ιβ'α} {k : κ} (hk : ) :
theorem uniformEquicontinuousOn_iInf_dom {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β' : Type u_10} [uα : ] {u : κ} {F : ιβ'α} {S : Set β'} {k : κ} (hk : ) :
theorem Filter.HasBasis.equicontinuousAt_iff_left {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {p : κProp} {s : κSet X} {F : ιXα} {x₀ : X} (hX : (nhds x₀).HasBasis p s) :
U, ∃ (k : κ), p k xs k, ∀ (i : ι), (F i x₀, F i x) U
theorem Filter.HasBasis.equicontinuousWithinAt_iff_left {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {p : κProp} {s : κSet X} {F : ιXα} {S : Set X} {x₀ : X} (hX : (nhdsWithin x₀ S).HasBasis p s) :
U, ∃ (k : κ), p k xs k, ∀ (i : ι), (F i x₀, F i x) U
theorem Filter.HasBasis.equicontinuousAt_iff_right {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {p : κProp} {s : κSet (α × α)} {F : ιXα} {x₀ : X} (hα : ().HasBasis p s) :
∀ (k : κ), p k∀ᶠ (x : X) in nhds x₀, ∀ (i : ι), (F i x₀, F i x) s k
theorem Filter.HasBasis.equicontinuousWithinAt_iff_right {ι : Type u_1} {κ : Type u_2} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {p : κProp} {s : κSet (α × α)} {F : ιXα} {S : Set X} {x₀ : X} (hα : ().HasBasis p s) :
∀ (k : κ), p k∀ᶠ (x : X) in nhdsWithin x₀ S, ∀ (i : ι), (F i x₀, F i x) s k
theorem Filter.HasBasis.equicontinuousAt_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {κ₁ : Type u_13} {κ₂ : Type u_14} {p₁ : κ₁Prop} {s₁ : κ₁Set X} {p₂ : κ₂Prop} {s₂ : κ₂Set (α × α)} {F : ιXα} {x₀ : X} (hX : (nhds x₀).HasBasis p₁ s₁) (hα : ().HasBasis p₂ s₂) :
∀ (k₂ : κ₂), p₂ k₂∃ (k₁ : κ₁), p₁ k₁ xs₁ k₁, ∀ (i : ι), (F i x₀, F i x) s₂ k₂
theorem Filter.HasBasis.equicontinuousWithinAt_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {κ₁ : Type u_13} {κ₂ : Type u_14} {p₁ : κ₁Prop} {s₁ : κ₁Set X} {p₂ : κ₂Prop} {s₂ : κ₂Set (α × α)} {F : ιXα} {S : Set X} {x₀ : X} (hX : (nhdsWithin x₀ S).HasBasis p₁ s₁) (hα : ().HasBasis p₂ s₂) :
∀ (k₂ : κ₂), p₂ k₂∃ (k₁ : κ₁), p₁ k₁ xs₁ k₁, ∀ (i : ι), (F i x₀, F i x) s₂ k₂
theorem Filter.HasBasis.uniformEquicontinuous_iff_left {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {p : κProp} {s : κSet (β × β)} {F : ιβα} (hβ : ().HasBasis p s) :
U, ∃ (k : κ), p k ∀ (x y : β), (x, y) s k∀ (i : ι), (F i x, F i y) U
theorem Filter.HasBasis.uniformEquicontinuousOn_iff_left {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {p : κProp} {s : κSet (β × β)} {F : ιβα} {S : Set β} (hβ : ( Filter.principal (S ×ˢ S)).HasBasis p s) :
U, ∃ (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_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {p : κProp} {s : κSet (α × α)} {F : ιβα} (hα : ().HasBasis p s) :
∀ (k : κ), p k∀ᶠ (xy : β × β) in , ∀ (i : ι), (F i xy.1, F i xy.2) s k
theorem Filter.HasBasis.uniformEquicontinuousOn_iff_right {ι : Type u_1} {κ : Type u_2} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {p : κProp} {s : κSet (α × α)} {F : ιβα} {S : Set β} (hα : ().HasBasis p s) :
∀ (k : κ), p k∀ᶠ (xy : β × β) in Filter.principal (S ×ˢ S), ∀ (i : ι), (F i xy.1, F i xy.2) s k
theorem Filter.HasBasis.uniformEquicontinuous_iff {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {κ₁ : Type u_13} {κ₂ : Type u_14} {p₁ : κ₁Prop} {s₁ : κ₁Set (β × β)} {p₂ : κ₂Prop} {s₂ : κ₂Set (α × α)} {F : ιβα} (hβ : ().HasBasis p₁ s₁) (hα : ().HasBasis p₂ s₂) :
∀ (k₂ : κ₂), p₂ k₂∃ (k₁ : κ₁), p₁ k₁ ∀ (x y : β), (x, y) s₁ k₁∀ (i : ι), (F i x, F i y) s₂ k₂
theorem Filter.HasBasis.uniformEquicontinuousOn_iff {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {κ₁ : Type u_13} {κ₂ : Type u_14} {p₁ : κ₁Prop} {s₁ : κ₁Set (β × β)} {p₂ : κ₂Prop} {s₂ : κ₂Set (α × α)} {F : ιβα} {S : Set β} (hβ : ( Filter.principal (S ×ˢ S)).HasBasis p₁ s₁) (hα : ().HasBasis p₂ s₂) :
∀ (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_7} {β : Type u_9} [tX : ] [uα : ] [uβ : ] {F : ιXα} {x₀ : X} {u : αβ} (hu : ) :
EquicontinuousAt ((fun (x : Xα) => u x) F) x₀

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

theorem UniformInducing.equicontinuousWithinAt_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} {β : Type u_9} [tX : ] [uα : ] [uβ : ] {F : ιXα} {S : Set X} {x₀ : X} {u : αβ} (hu : ) :
EquicontinuousWithinAt ((fun (x : Xα) => u x) F) S x₀

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

theorem UniformInducing.equicontinuous_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} {β : Type u_9} [tX : ] [uα : ] [uβ : ] {F : ιXα} {u : αβ} (hu : ) :
Equicontinuous ((fun (x : Xα) => u x) F)

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

theorem UniformInducing.equicontinuousOn_iff {ι : Type u_1} {X : Type u_3} {α : Type u_7} {β : Type u_9} [tX : ] [uα : ] [uβ : ] {F : ιXα} {S : Set X} {u : αβ} (hu : ) :
EquicontinuousOn ((fun (x : Xα) => u x) F) S

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

theorem UniformInducing.uniformEquicontinuous_iff {ι : Type u_1} {α : Type u_7} {β : Type u_9} {γ : Type u_11} [uα : ] [uβ : ] [uγ : ] {F : ιβα} {u : αγ} (hu : ) :
UniformEquicontinuous ((fun (x : βα) => u x) F)

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

theorem UniformInducing.uniformEquicontinuousOn_iff {ι : Type u_1} {α : Type u_7} {β : Type u_9} {γ : Type u_11} [uα : ] [uβ : ] [uγ : ] {F : ιβα} {S : Set β} {u : αγ} (hu : ) :
UniformEquicontinuousOn ((fun (x : βα) => u x) F) S

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

theorem EquicontinuousWithinAt.closure' {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : ] [tY : ] [uα : ] {A : Set Y} {u : YXα} {S : Set X} {x₀ : X} (hA : EquicontinuousWithinAt (u Subtype.val) S x₀) (hu₁ : Continuous (S.restrict u)) (hu₂ : Continuous ( u)) :
EquicontinuousWithinAt (u Subtype.val) S x₀

If a set of functions is equicontinuous at some x₀ within a set S, the same is true for its closure in any topology for which evaluation at any x ∈ S ∪ {x₀} is continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to X → α satisfying the right continuity conditions. See also Set.EquicontinuousWithinAt.closure for a more familiar (but weaker) statement.

Note: This could technically be called EquicontinuousWithinAt.closure without name clashes with Set.EquicontinuousWithinAt.closure, but we don't do it because, even with a protected marker, it would introduce ambiguities while working in namespace Set (e.g, in the proof of any theorem called Set.something).

theorem EquicontinuousAt.closure' {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : ] [tY : ] [uα : ] {A : Set Y} {u : YXα} {x₀ : X} (hA : EquicontinuousAt (u Subtype.val) x₀) (hu : ) :
EquicontinuousAt (u Subtype.val) x₀

If a set of functions is equicontinuous at some x₀, the same is true for its closure in any topology for which evaluation at any point is continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to X → α satisfying the right continuity conditions. See also Set.EquicontinuousAt.closure for a more familiar statement.

theorem Set.EquicontinuousAt.closure {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {A : Set (Xα)} {x₀ : X} (hA : A.EquicontinuousAt x₀) :
().EquicontinuousAt x₀

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

theorem Set.EquicontinuousWithinAt.closure {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {A : Set (Xα)} {S : Set X} {x₀ : X} (hA : A.EquicontinuousWithinAt S x₀) :
().EquicontinuousWithinAt S x₀

If a set of functions is equicontinuous at some x₀ within a set S, its closure for the product topology is also equicontinuous at x₀ within S. This would also be true for the coarser topology of pointwise convergence on S ∪ {x₀}, see Set.EquicontinuousWithinAt.closure'.

theorem Equicontinuous.closure' {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : ] [tY : ] [uα : ] {A : Set Y} {u : YXα} (hA : Equicontinuous (u Subtype.val)) (hu : ) :
Equicontinuous (u Subtype.val)

If a set of functions is equicontinuous, the same is true for its closure in any topology for which evaluation at any point is continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to X → α satisfying the right continuity conditions. See also Set.Equicontinuous.closure for a more familiar statement.

theorem EquicontinuousOn.closure' {X : Type u_3} {Y : Type u_5} {α : Type u_7} [tX : ] [tY : ] [uα : ] {A : Set Y} {u : YXα} {S : Set X} (hA : EquicontinuousOn (u Subtype.val) S) (hu : Continuous (S.restrict u)) :
EquicontinuousOn (u Subtype.val) S

If a set of functions is equicontinuous on a set S, the same is true for its closure in any topology for which evaluation at any x ∈ S is continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to X → α satisfying the right continuity conditions. See also Set.EquicontinuousOn.closure for a more familiar (but weaker) statement.

theorem Set.Equicontinuous.closure {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {A : Set (Xα)} (hA : A.Equicontinuous) :
().Equicontinuous

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

theorem Set.EquicontinuousOn.closure {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {A : Set (Xα)} {S : Set X} (hA : A.EquicontinuousOn S) :
().EquicontinuousOn S

If a set of functions is equicontinuous, its closure for the product topology is also equicontinuous. This would also be true for the coarser topology of pointwise convergence on S, see EquicontinuousOn.closure'.

theorem UniformEquicontinuousOn.closure' {Y : Type u_5} {α : Type u_7} {β : Type u_9} [tY : ] [uα : ] [uβ : ] {A : Set Y} {u : Yβα} {S : Set β} (hA : UniformEquicontinuousOn (u Subtype.val) S) (hu : Continuous (S.restrict u)) :
UniformEquicontinuousOn (u Subtype.val) S

If a set of functions is uniformly equicontinuous on a set S, the same is true for its closure in any topology for which evaluation at any x ∈ S i continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to β → α satisfying the right continuity conditions. See also Set.UniformEquicontinuousOn.closure for a more familiar (but weaker) statement.

theorem UniformEquicontinuous.closure' {Y : Type u_5} {α : Type u_7} {β : Type u_9} [tY : ] [uα : ] [uβ : ] {A : Set Y} {u : Yβα} (hA : UniformEquicontinuous (u Subtype.val)) (hu : ) :
UniformEquicontinuous (u Subtype.val)

If a set of functions is uniformly equicontinuous, the same is true for its closure in any topology for which evaluation at any point is continuous. Since this will be applied to DFunLike types, we state it for any topological space whith a map to β → α satisfying the right continuity conditions. See also Set.UniformEquicontinuous.closure for a more familiar statement.

theorem Set.UniformEquicontinuous.closure {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {A : Set (βα)} (hA : A.UniformEquicontinuous) :
().UniformEquicontinuous

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

theorem Set.UniformEquicontinuousOn.closure {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {A : Set (βα)} {S : Set β} (hA : A.UniformEquicontinuousOn S) :
().UniformEquicontinuousOn S

If a set of functions is uniformly equicontinuous on a set S, its closure for the product topology is also uniformly equicontinuous. This would also be true for the coarser topology of pointwise convergence on S, see UniformEquicontinuousOn.closure'.

theorem Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {l : } [l.NeBot] {F : ιXα} {f : Xα} {S : Set X} {x₀ : X} (h₁ : xS, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) l (nhds (f x))) (h₂ : Filter.Tendsto (fun (x : ι) => F x x₀) l (nhds (f x₀))) (h₃ : ) :

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

theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {l : } [l.NeBot] {F : ιXα} {f : Xα} {x₀ : X} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : ) :

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 Filter.Tendsto.continuous_of_equicontinuous {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {l : } [l.NeBot] {F : ιXα} {f : Xα} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : ) :

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

theorem Filter.Tendsto.continuousOn_of_equicontinuousOn {ι : Type u_1} {X : Type u_3} {α : Type u_7} [tX : ] [uα : ] {l : } [l.NeBot] {F : ιXα} {f : Xα} {S : Set X} (h₁ : xS, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) l (nhds (f x))) (h₂ : ) :

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

theorem Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {l : } [l.NeBot] {F : ιβα} {f : βα} {S : Set β} (h₁ : xS, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) l (nhds (f x))) (h₂ : ) :

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

theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {ι : Type u_1} {α : Type u_7} {β : Type u_9} [uα : ] [uβ : ] {l : } [l.NeBot] {F : ιβα} {f : βα} (h₁ : Filter.Tendsto F l (nhds f)) (h₂ : ) :

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_7} [tX : ] [uα : ] {l : } {F : ιXα} {f : Xα} {s : Set X} {x : X} {z : α} (hF : ) (hf : Filter.Tendsto f () (nhds z)) (hs : ys, Filter.Tendsto (fun (x : ι) => F x y) l (nhds (f y))) (hx : x ) :
Filter.Tendsto (fun (x_1 : ι) => F x_1 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_7} [tX : ] [uα : ] {l : } {F : ιXα} {f : Xα} (hF : ) (hf : ) :
IsClosed {x : 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.