Uniform convergence

A sequence of functions Fₙ (with values in a metric space) converges uniformly on a set s to a function f if, for all ε > 0, for all large enough n, one has for all y ∈ s the inequality dist (f y, Fₙ y) < ε. Under uniform convergence, many properties of the Fₙ pass to the limit, most notably continuity. We prove this in the file, defining the notion of uniform convergence in the more general setting of uniform spaces, and with respect to an arbitrary indexing set endowed with a filter (instead of just ℕ with atTop).

Main results

Let α be a topological space, β a uniform space, Fₙ and f be functions from α to β (where the index n belongs to an indexing type ι endowed with a filter p).

• TendstoUniformlyOn F f p s: the fact that Fₙ converges uniformly to f on s. This means that, for any entourage u of the diagonal, for large enough n (with respect to p), one has (f y, Fₙ y) ∈ u for all y ∈ s.
• TendstoUniformly F f p: same notion with s = univ.
• TendstoUniformlyOn.continuousOn: a uniform limit on a set of functions which are continuous on this set is itself continuous on this set.
• TendstoUniformly.continuous: a uniform limit of continuous functions is continuous.
• TendstoUniformlyOn.tendsto_comp: If Fₙ tends uniformly to f on a set s, and gₙ tends to x within s, then Fₙ gₙ tends to f x if f is continuous at x within s.
• TendstoUniformly.tendsto_comp: If Fₙ tends uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.

We also define notions where the convergence is locally uniform, called TendstoLocallyUniformlyOn F f p s and TendstoLocallyUniformly F f p. The previous theorems all have corresponding versions under locally uniform convergence.

Finally, we introduce the notion of a uniform Cauchy sequence, which is to uniform convergence what a Cauchy sequence is to the usual notion of convergence.

Implementation notes

We derive most of our initial results from an auxiliary definition TendstoUniformlyOnFilter. This definition in and of itself can sometimes be useful, e.g., when studying the local behavior of the Fₙ near a point, which would typically look like TendstoUniformlyOnFilter F f p (𝓝 x). Still, while this may be the "correct" definition (see tendstoUniformlyOn_iff_tendstoUniformlyOnFilter), it is somewhat unwieldy to work with in practice. Thus, we provide the more traditional definition in TendstoUniformlyOn.

Most results hold under weaker assumptions of locally uniform approximation. In a first section, we prove the results under these weaker assumptions. Then, we derive the results on uniform convergence from them.

Tags

Uniform limit, uniform convergence, tends uniformly to

Different notions of uniform convergence

We define uniform convergence and locally uniform convergence, on a set or in the whole space.

def TendstoUniformlyOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) (p' : Filter α) : Prop

A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f with respect to the filter p if, for any entourage of the diagonal u, one has p ×ˢ p'-eventually (f x, Fₙ x) ∈ u.

Equations

• TendstoUniformlyOnFilter F f p p' = ∀ u ∈ uniformity β, ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u

theorem tendstoUniformlyOnFilter_iff_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} : TendstoUniformlyOnFilter F f p p' ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ p') (uniformity β)

A sequence of functions Fₙ converges uniformly on a filter p' to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ p' to the uniformity. In other words: one knows nothing about the behavior of x in this limit besides it being in p'.

def TendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) : Prop

A sequence of functions Fₙ converges uniformly on a set s to a limiting function f with respect to the filter p if, for any entourage of the diagonal u, one has p-eventually (f x, Fₙ x) ∈ u for all x ∈ s.

Equations

• TendstoUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ x ∈ s, (f x, F n x) ∈ u

theorem tendstoUniformlyOn_iff_tendstoUniformlyOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s ↔ TendstoUniformlyOnFilter F f p (Filter.principal s)

theorem TendstoUniformlyOnFilter.tendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOnFilter F f p (Filter.principal s) → TendstoUniformlyOn F f p s

Alias of the reverse direction of tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.

theorem TendstoUniformlyOn.tendstoUniformlyOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s → TendstoUniformlyOnFilter F f p (Filter.principal s)

Alias of the forward direction of tendstoUniformlyOn_iff_tendstoUniformlyOnFilter.

theorem tendstoUniformlyOn_iff_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {s : Set α} : TendstoUniformlyOn F f p s ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ Filter.principal s) (uniformity β)

A sequence of functions Fₙ converges uniformly on a set s to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ 𝓟 s to the uniformity. In other words: one knows nothing about the behavior of x in this limit besides it being in s.

def TendstoUniformly {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι) : Prop

A sequence of functions Fₙ converges uniformly to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, one has p-eventually (f x, Fₙ x) ∈ u for all x.

Equations

• TendstoUniformly F f p = ∀ u ∈ uniformity β, ∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ u

theorem tendstoUniformlyOn_univ {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformlyOn F f p Set.univ ↔ TendstoUniformly F f p

theorem tendstoUniformly_iff_tendstoUniformlyOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformly F f p ↔ TendstoUniformlyOnFilter F f p ⊤

theorem TendstoUniformly.tendstoUniformlyOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) : TendstoUniformlyOnFilter F f p ⊤

theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} : TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun (i : ι) (x : ↑s) => F i ↑x) (f ∘ Subtype.val) p

theorem tendstoUniformly_iff_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformly F f p ↔ Filter.Tendsto (fun (q : ι × α) => (f q.2, F q.1 q.2)) (p ×ˢ ⊤) (uniformity β)

A sequence of functions Fₙ converges uniformly to a limiting function f w.r.t. filter p iff the function (n, x) ↦ (f x, Fₙ x) converges along p ×ˢ ⊤ to the uniformity. In other words: one knows nothing about the behavior of x in this limit.

theorem TendstoUniformlyOnFilter.tendsto_at {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {p' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hx : Filter.principal {x} ≤ p') : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem TendstoUniformlyOn.tendsto_at {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) {x : α} (hx : x ∈ s) : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem TendstoUniformly.tendsto_at {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) (x : α) : Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem TendstoUniformlyOnFilter.mono_left {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter ι} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p) : TendstoUniformlyOnFilter F f p'' p'

theorem TendstoUniformlyOnFilter.mono_right {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (hp : p'' ≤ p') : TendstoUniformlyOnFilter F f p p''

theorem TendstoUniformlyOn.mono {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {s' : Set α} (h : TendstoUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoUniformlyOn F f p s'

theorem TendstoUniformlyOnFilter.congr {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p') (hff' : ∀ᶠ (n : ι × α) in p ×ˢ p', F n.1 n.2 = F' n.1 n.2) : TendstoUniformlyOnFilter F' f p p'

theorem TendstoUniformlyOn.congr {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {F' : ι → α → β} (hf : TendstoUniformlyOn F f p s) (hff' : ∀ᶠ (n : ι) in p, Set.EqOn (F n) (F' n) s) : TendstoUniformlyOn F' f p s

theorem TendstoUniformlyOn.congr_right {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {g : α → β} (hf : TendstoUniformlyOn F f p s) (hfg : Set.EqOn f g s) : TendstoUniformlyOn F g p s

theorem TendstoUniformly.tendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformly F f p) : TendstoUniformlyOn F f p s

theorem TendstoUniformlyOnFilter.comp {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (h : TendstoUniformlyOnFilter F f p p') (g : γ → α) : TendstoUniformlyOnFilter (fun (n : ι) => F n ∘ g) (f ∘ g) p (Filter.comap g p')

Composing on the right by a function preserves uniform convergence on a filter

theorem TendstoUniformlyOn.comp {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (h : TendstoUniformlyOn F f p s) (g : γ → α) : TendstoUniformlyOn (fun (n : ι) => F n ∘ g) (f ∘ g) p (g ⁻¹' s)

Composing on the right by a function preserves uniform convergence on a set

theorem TendstoUniformly.comp {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (h : TendstoUniformly F f p) (g : γ → α) : TendstoUniformly (fun (n : ι) => F n ∘ g) (f ∘ g) p

Composing on the right by a function preserves uniform convergence

theorem UniformContinuous.comp_tendstoUniformlyOnFilter {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOnFilter F f p p') : TendstoUniformlyOnFilter (fun (i : ι) => g ∘ F i) (g ∘ f) p p'

Composing on the left by a uniformly continuous function preserves uniform convergence on a filter

theorem UniformContinuous.comp_tendstoUniformlyOn {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformlyOn F f p s) : TendstoUniformlyOn (fun (i : ι) => g ∘ F i) (g ∘ f) p s

Composing on the left by a uniformly continuous function preserves uniform convergence on a set

theorem UniformContinuous.comp_tendstoUniformly {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (h : TendstoUniformly F f p) : TendstoUniformly (fun (i : ι) => g ∘ F i) (g ∘ f) p

Composing on the left by a uniformly continuous function preserves uniform convergence

theorem TendstoUniformlyOnFilter.prod_map {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_1} {α' : Type u_2} {β' : Type u_3} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : Filter ι'} {q' : Filter α'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q q') : TendstoUniformlyOnFilter (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ q) (p' ×ˢ q')

theorem TendstoUniformlyOn.prod_map {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_1} {α' : Type u_2} {β' : Type u_3} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} {s' : Set α'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s') : TendstoUniformlyOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p') (s ×ˢ s')

theorem TendstoUniformly.prod_map {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_1} {α' : Type u_2} {β' : Type u_3} [UniformSpace β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (Prod.map f f') (p ×ˢ p')

theorem TendstoUniformlyOnFilter.prod {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} {ι' : Type u_1} {β' : Type u_2} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {q : Filter ι'} (h : TendstoUniformlyOnFilter F f p p') (h' : TendstoUniformlyOnFilter F' f' q p') : TendstoUniformlyOnFilter (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ q) p'

theorem TendstoUniformlyOn.prod {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {ι' : Type u_1} {β' : Type u_2} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p' s) : TendstoUniformlyOn (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p.prod p') s

theorem TendstoUniformly.prod {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {ι' : Type u_1} {β' : Type u_2} [UniformSpace β'] {F' : ι' → α → β'} {f' : α → β'} {p' : Filter ι'} (h : TendstoUniformly F f p) (h' : TendstoUniformly F' f' p') : TendstoUniformly (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (fun (a : α) => (f a, f' a)) (p ×ˢ p')

theorem tendsto_prod_filter_iff {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {c : β} : Filter.Tendsto (↿F) (p ×ˢ p') (nhds c) ↔ TendstoUniformlyOnFilter F (fun (x : α) => c) p p'

Uniform convergence on a filter p' to a constant function is equivalent to convergence in p ×ˢ p'.

theorem tendsto_prod_principal_iff {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {c : β} : Filter.Tendsto (↿F) (p ×ˢ Filter.principal s) (nhds c) ↔ TendstoUniformlyOn F (fun (x : α) => c) p s

Uniform convergence on a set s to a constant function is equivalent to convergence in p ×ˢ 𝓟 s.

theorem tendsto_prod_top_iff {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {c : β} : Filter.Tendsto (↿F) (p ×ˢ ⊤) (nhds c) ↔ TendstoUniformly F (fun (x : α) => c) p

Uniform convergence to a constant function is equivalent to convergence in p ×ˢ ⊤.

theorem tendstoUniformlyOn_empty {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} : TendstoUniformlyOn F f p ∅

Uniform convergence on the empty set is vacuously true

theorem tendstoUniformlyOn_singleton_iff_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} : TendstoUniformlyOn F f p {x} ↔ Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))

Uniform convergence on a singleton is equivalent to regular convergence

theorem Filter.Tendsto.tendstoUniformlyOnFilter_const {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {p : Filter ι} {g : ι → β} {b : β} (hg : Filter.Tendsto g p (nhds b)) (p' : Filter α) : TendstoUniformlyOnFilter (fun (n : ι) (x : α) => g n) (fun (x : α) => b) p p'

If a sequence g converges to some b, then the sequence of constant functions fun n ↦ fun a ↦ g n converges to the constant function fun a ↦ b on any set s

theorem Filter.Tendsto.tendstoUniformlyOn_const {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {p : Filter ι} {g : ι → β} {b : β} (hg : Filter.Tendsto g p (nhds b)) (s : Set α) : TendstoUniformlyOn (fun (n : ι) (x : α) => g n) (fun (x : α) => b) p s

If a sequence g converges to some b, then the sequence of constant functions fun n ↦ fun a ↦ g n converges to the constant function fun a ↦ b on any set s

theorem UniformContinuousOn.tendstoUniformlyOn {α : Type u} {β : Type v} {γ : Type w} [UniformSpace β] [UniformSpace α] [UniformSpace γ] {x : α} {U : Set α} {V : Set β} {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ V)) (hU : x ∈ U) : TendstoUniformlyOn F (F x) (nhdsWithin x U) V

theorem UniformContinuousOn.tendstoUniformly {α : Type u} {β : Type v} {γ : Type w} [UniformSpace β] [UniformSpace α] [UniformSpace γ] {x : α} {U : Set α} (hU : U ∈ nhds x) {F : α → β → γ} (hF : UniformContinuousOn (↿F) (U ×ˢ Set.univ)) : TendstoUniformly F (F x) (nhds x)

theorem UniformContinuous₂.tendstoUniformly {α : Type u} {β : Type v} {γ : Type w} [UniformSpace β] [UniformSpace α] [UniformSpace γ] {f : α → β → γ} (h : UniformContinuous₂ f) {x : α} : TendstoUniformly f (f x) (nhds x)

def UniformCauchySeqOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] (F : ι → α → β) (p : Filter ι) (p' : Filter α) : Prop

A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded

Equations

• UniformCauchySeqOnFilter F p p' = ∀ u ∈ uniformity β, ∀ᶠ (m : (ι × ι) × α) in (p ×ˢ p) ×ˢ p', (F m.1.1 m.2, F m.1.2 m.2) ∈ u

def UniformCauchySeqOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] (F : ι → α → β) (p : Filter ι) (s : Set α) : Prop

A sequence is uniformly Cauchy if eventually all of its pairwise differences are uniformly bounded

Equations

• UniformCauchySeqOn F p s = ∀ u ∈ uniformity β, ∀ᶠ (m : ι × ι) in p ×ˢ p, ∀ x ∈ s, (F m.1 x, F m.2 x) ∈ u

theorem uniformCauchySeqOn_iff_uniformCauchySeqOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} : UniformCauchySeqOn F p s ↔ UniformCauchySeqOnFilter F p (Filter.principal s)

theorem UniformCauchySeqOn.uniformCauchySeqOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} (hF : UniformCauchySeqOn F p s) : UniformCauchySeqOnFilter F p (Filter.principal s)

theorem TendstoUniformlyOnFilter.uniformCauchySeqOnFilter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (hF : TendstoUniformlyOnFilter F f p p') : UniformCauchySeqOnFilter F p p'

A sequence that converges uniformly is also uniformly Cauchy

theorem TendstoUniformlyOn.uniformCauchySeqOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hF : TendstoUniformlyOn F f p s) : UniformCauchySeqOn F p s

A sequence that converges uniformly is also uniformly Cauchy

theorem UniformCauchySeqOnFilter.tendstoUniformlyOnFilter_of_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} (hF : UniformCauchySeqOnFilter F p p') (hF' : ∀ᶠ (x : α) in p', Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))) : TendstoUniformlyOnFilter F f p p'

A uniformly Cauchy sequence converges uniformly to its limit

theorem UniformCauchySeqOn.tendstoUniformlyOn_of_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (hF : UniformCauchySeqOn F p s) (hF' : ∀ x ∈ s, Filter.Tendsto (fun (n : ι) => F n x) p (nhds (f x))) : TendstoUniformlyOn F f p s

A uniformly Cauchy sequence converges uniformly to its limit

theorem UniformCauchySeqOnFilter.mono_left {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter ι} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p) : UniformCauchySeqOnFilter F p'' p'

theorem UniformCauchySeqOnFilter.mono_right {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {p'' : Filter α} (hf : UniformCauchySeqOnFilter F p p') (hp : p'' ≤ p') : UniformCauchySeqOnFilter F p p''

theorem UniformCauchySeqOn.mono {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {s' : Set α} (hf : UniformCauchySeqOn F p s) (hss' : s' ⊆ s) : UniformCauchySeqOn F p s'

theorem UniformCauchySeqOnFilter.comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {p : Filter ι} {p' : Filter α} {γ : Type u_1} (hf : UniformCauchySeqOnFilter F p p') (g : γ → α) : UniformCauchySeqOnFilter (fun (n : ι) => F n ∘ g) p (Filter.comap g p')

Composing on the right by a function preserves uniform Cauchy sequences

theorem UniformCauchySeqOn.comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {γ : Type u_1} (hf : UniformCauchySeqOn F p s) (g : γ → α) : UniformCauchySeqOn (fun (n : ι) => F n ∘ g) p (g ⁻¹' s)

Composing on the right by a function preserves uniform Cauchy sequences

theorem UniformContinuous.comp_uniformCauchySeqOn {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} [UniformSpace γ] {g : β → γ} (hg : UniformContinuous g) (hf : UniformCauchySeqOn F p s) : UniformCauchySeqOn (fun (n : ι) => g ∘ F n) p s

Composing on the left by a uniformly continuous function preserves uniform Cauchy sequences

theorem UniformCauchySeqOn.prod_map {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_1} {α' : Type u_2} {β' : Type u_3} [UniformSpace β'] {F' : ι' → α' → β'} {p' : Filter ι'} {s' : Set α'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s') : UniformCauchySeqOn (fun (i : ι × ι') => Prod.map (F i.1) (F' i.2)) (p ×ˢ p') (s ×ˢ s')

theorem UniformCauchySeqOn.prod {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {ι' : Type u_1} {β' : Type u_2} [UniformSpace β'] {F' : ι' → α → β'} {p' : Filter ι'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p' s) : UniformCauchySeqOn (fun (i : ι × ι') (a : α) => (F i.1 a, F' i.2 a)) (p ×ˢ p') s

theorem UniformCauchySeqOn.prod' {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι} {β' : Type u_1} [UniformSpace β'] {F' : ι → α → β'} (h : UniformCauchySeqOn F p s) (h' : UniformCauchySeqOn F' p s) : UniformCauchySeqOn (fun (i : ι) (a : α) => (F i a, F' i a)) p s

theorem UniformCauchySeqOn.cauchy_map {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} {p : Filter ι} [hp : p.NeBot] (hf : UniformCauchySeqOn F p s) (hx : x ∈ s) : Cauchy (Filter.map (fun (i : ι) => F i x) p)

If a sequence of functions is uniformly Cauchy on a set, then the values at each point form a Cauchy sequence.

theorem UniformCauchySeqOn.cauchySeq {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {s : Set α} {x : α} [Nonempty ι] [SemilatticeSup ι] (hf : UniformCauchySeqOn F Filter.atTop s) (hx : x ∈ s) : CauchySeq fun (i : ι) => F i x

If a sequence of functions is uniformly Cauchy on a set, then the values at each point form a Cauchy sequence. See UniformCauchSeqOn.cauchy_map for the non-atTop case.

theorem tendstoUniformlyOn_of_seq_tendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} [l.IsCountablyGenerated] (h : ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s) : TendstoUniformlyOn F f l s

theorem TendstoUniformlyOn.seq_tendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} (h : TendstoUniformlyOn F f l s) (u : ℕ → ι) (hu : Filter.Tendsto u Filter.atTop l) : TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s

theorem tendstoUniformlyOn_iff_seq_tendstoUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {l : Filter ι} [l.IsCountablyGenerated] : TendstoUniformlyOn F f l s ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformlyOn (fun (n : ℕ) => F (u n)) f Filter.atTop s

theorem tendstoUniformly_iff_seq_tendstoUniformly {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {l : Filter ι} [l.IsCountablyGenerated] : TendstoUniformly F f l ↔ ∀ (u : ℕ → ι), Filter.Tendsto u Filter.atTop l → TendstoUniformly (fun (n : ℕ) => F (u n)) f Filter.atTop

theorem TendstoUniformlyOnFilter.tendsto_of_eventually_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformlyOnFilter F f p p') (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)

theorem TendstoUniformly.tendsto_of_eventually_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} {p' : Filter α} [p.NeBot] {L : ι → β} {ℓ : β} (h1 : TendstoUniformly F f p) (h2 : ∀ᶠ (i : ι) in p, Filter.Tendsto (F i) p' (nhds (L i))) (h3 : Filter.Tendsto L p (nhds ℓ)) : Filter.Tendsto f p' (nhds ℓ)

def TendstoLocallyUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] [TopologicalSpace α] (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) : Prop

A sequence of functions Fₙ converges locally uniformly on a set s to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, for any x ∈ s, one has p-eventually (f y, Fₙ y) ∈ u for all y in a neighborhood of x in s.

Equations

• TendstoLocallyUniformlyOn F f p s = ∀ u ∈ uniformity β, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

def TendstoLocallyUniformly {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] [TopologicalSpace α] (F : ι → α → β) (f : α → β) (p : Filter ι) : Prop

A sequence of functions Fₙ converges locally uniformly to a limiting function f with respect to a filter p if, for any entourage of the diagonal u, for any x, one has p-eventually (f y, Fₙ y) ∈ u for all y in a neighborhood of x.

Equations

• TendstoLocallyUniformly F f p = ∀ u ∈ uniformity β, ∀ (x : α), ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u

theorem tendstoLocallyUniformlyOn_univ {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformlyOn F f p Set.univ ↔ TendstoLocallyUniformly F f p

theorem tendstoLocallyUniformlyOn_iff_forall_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhdsWithin x s) (uniformity β)

theorem IsOpen.tendstoLocallyUniformlyOn_iff_forall_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (hs : IsOpen s) : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)

theorem tendstoLocallyUniformly_iff_forall_tendsto {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformly F f p ↔ ∀ (x : α), Filter.Tendsto (fun (y : ι × α) => (f y.2, F y.1 y.2)) (p ×ˢ nhds x) (uniformity β)

theorem tendstoLocallyUniformlyOn_iff_tendstoLocallyUniformly_comp_coe {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformlyOn F f p s ↔ TendstoLocallyUniformly (fun (i : ι) (x : ↑s) => F i ↑x) (f ∘ Subtype.val) p

theorem TendstoUniformlyOn.tendstoLocallyUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (h : TendstoUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p s

theorem TendstoUniformly.tendstoLocallyUniformly {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] (h : TendstoUniformly F f p) : TendstoLocallyUniformly F f p

theorem TendstoLocallyUniformlyOn.mono {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {s' : Set α} {p : Filter ι} [TopologicalSpace α] (h : TendstoLocallyUniformlyOn F f p s) (h' : s' ⊆ s) : TendstoLocallyUniformlyOn F f p s'

theorem tendstoLocallyUniformlyOn_iUnion {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] {ι' : Sort u_1} {S : ι' → Set α} (hS : ∀ (i : ι'), IsOpen (S i)) (h : ∀ (i : ι'), TendstoLocallyUniformlyOn F f p (S i)) : TendstoLocallyUniformlyOn F f p (⋃ (i : ι'), S i)

theorem tendstoLocallyUniformlyOn_biUnion {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] {s : Set γ} {S : γ → Set α} (hS : ∀ i ∈ s, IsOpen (S i)) (h : ∀ i ∈ s, TendstoLocallyUniformlyOn F f p (S i)) : TendstoLocallyUniformlyOn F f p (⋃ i ∈ s, S i)

theorem tendstoLocallyUniformlyOn_sUnion {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s) (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S)

theorem TendstoLocallyUniformlyOn.union {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] {s₁ : Set α} {s₂ : Set α} (hs₁ : IsOpen s₁) (hs₂ : IsOpen s₂) (h₁ : TendstoLocallyUniformlyOn F f p s₁) (h₂ : TendstoLocallyUniformlyOn F f p s₂) : TendstoLocallyUniformlyOn F f p (s₁ ∪ s₂)

theorem TendstoLocallyUniformly.tendstoLocallyUniformlyOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (h : TendstoLocallyUniformly F f p) : TendstoLocallyUniformlyOn F f p s

theorem tendstoLocallyUniformly_iff_tendstoUniformly_of_compactSpace {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] [CompactSpace α] : TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p

On a compact space, locally uniform convergence is just uniform convergence.

theorem tendstoLocallyUniformlyOn_iff_tendstoUniformlyOn_of_compact {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (hs : IsCompact s) : TendstoLocallyUniformlyOn F f p s ↔ TendstoUniformlyOn F f p s

For a compact set s, locally uniform convergence on s is just uniform convergence on s.

theorem TendstoLocallyUniformlyOn.comp {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] [TopologicalSpace γ] {t : Set γ} (h : TendstoLocallyUniformlyOn F f p s) (g : γ → α) (hg : Set.MapsTo g t s) (cg : ContinuousOn g t) : TendstoLocallyUniformlyOn (fun (n : ι) => F n ∘ g) (f ∘ g) p t

theorem TendstoLocallyUniformly.comp {α : Type u} {β : Type v} {γ : Type w} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] [TopologicalSpace γ] (h : TendstoLocallyUniformly F f p) (g : γ → α) (cg : Continuous g) : TendstoLocallyUniformly (fun (n : ι) => F n ∘ g) (f ∘ g) p

theorem tendstoLocallyUniformlyOn_TFAE {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {s : Set α} [TopologicalSpace α] [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι) (hs : IsOpen s) : [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ nhdsWithin x s, TendstoUniformlyOn G g p v].TFAE

theorem tendstoLocallyUniformlyOn_iff_forall_isCompact {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] [LocallyCompactSpace α] (hs : IsOpen s) : TendstoLocallyUniformlyOn F f p s ↔ ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn F f p K

theorem tendstoLocallyUniformly_iff_forall_isCompact {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] [LocallyCompactSpace α] : TendstoLocallyUniformly F f p ↔ ∀ (K : Set α), IsCompact K → TendstoUniformlyOn F f p K

theorem tendstoLocallyUniformlyOn_iff_filter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (nhdsWithin x s)

theorem tendstoLocallyUniformly_iff_filter {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] : TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (nhds x)

theorem TendstoLocallyUniformlyOn.tendsto_at {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (hf : TendstoLocallyUniformlyOn F f p s) {a : α} (ha : a ∈ s) : Filter.Tendsto (fun (i : ι) => F i a) p (nhds (f a))

theorem TendstoLocallyUniformlyOn.unique {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] [p.NeBot] [T2Space β] {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : TendstoLocallyUniformlyOn F g p s) : Set.EqOn f g s

theorem TendstoLocallyUniformlyOn.congr {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : ∀ (n : ι), Set.EqOn (F n) (G n) s) : TendstoLocallyUniformlyOn G f p s

theorem TendstoLocallyUniformlyOn.congr_right {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : Set.EqOn f g s) : TendstoLocallyUniformlyOn F g p s

Uniform approximation

In this section, we give lemmas ensuring that a function is continuous if it can be approximated uniformly by continuous functions. We give various versions, within a set or the whole space, at a single point or at all points, with locally uniform approximation or uniform approximation. All the statements are derived from a statement about locally uniform approximation within a set at a point, called continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt.

theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} {s : Set α} {x : α} [TopologicalSpace α] (hx : x ∈ s) (L : ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousWithinAt f s x

A function which can be locally uniformly approximated by functions which are continuous within a set at a point is continuous within this set at this point.

theorem continuousAt_of_locally_uniform_approx_of_continuousAt {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} {x : α} [TopologicalSpace α] (L : ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousAt f x

A function which can be locally uniformly approximated by functions which are continuous at a point is continuous at this point.

theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} {s : Set α} [TopologicalSpace α] (L : ∀ x ∈ s, ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∃ (F : α → β), ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : ContinuousOn f s

A function which can be locally uniformly approximated by functions which are continuous on a set is continuous on this set.

theorem continuousOn_of_uniform_approx_of_continuousOn {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} {s : Set α} [TopologicalSpace α] (L : ∀ u ∈ uniformity β, ∃ (F : α → β), ContinuousOn F s ∧ ∀ y ∈ s, (f y, F y) ∈ u) : ContinuousOn f s

A function which can be uniformly approximated by functions which are continuous on a set is continuous on this set.

theorem continuous_of_locally_uniform_approx_of_continuousAt {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} [TopologicalSpace α] (L : ∀ (x : α), ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∃ (F : α → β), ContinuousAt F x ∧ ∀ y ∈ t, (f y, F y) ∈ u) : Continuous f

A function which can be locally uniformly approximated by continuous functions is continuous.

theorem continuous_of_uniform_approx_of_continuous {α : Type u} {β : Type v} [UniformSpace β] {f : α → β} [TopologicalSpace α] (L : ∀ u ∈ uniformity β, ∃ (F : α → β), Continuous F ∧ ∀ (y : α), (f y, F y) ∈ u) : Continuous f

A function which can be uniformly approximated by continuous functions is continuous.

Uniform limits

From the previous statements on uniform approximation, we deduce continuity results for uniform limits.

theorem TendstoLocallyUniformlyOn.continuousOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (h : TendstoLocallyUniformlyOn F f p s) (hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s) [p.NeBot] : ContinuousOn f s

A locally uniform limit on a set of functions which are continuous on this set is itself continuous on this set.

theorem TendstoUniformlyOn.continuousOn {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [TopologicalSpace α] (h : TendstoUniformlyOn F f p s) (hc : ∀ᶠ (n : ι) in p, ContinuousOn (F n) s) [p.NeBot] : ContinuousOn f s

A uniform limit on a set of functions which are continuous on this set is itself continuous on this set.

theorem TendstoLocallyUniformly.continuous {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] (h : TendstoLocallyUniformly F f p) (hc : ∀ᶠ (n : ι) in p, Continuous (F n)) [p.NeBot] : Continuous f

A locally uniform limit of continuous functions is continuous.

theorem TendstoUniformly.continuous {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} [TopologicalSpace α] (h : TendstoUniformly F f p) (hc : ∀ᶠ (n : ι) in p, Continuous (F n)) [p.NeBot] : Continuous f

A uniform limit of continuous functions is continuous.

Composing limits under uniform convergence

In general, if Fₙ converges pointwise to a function f, and gₙ tends to x, it is not true that Fₙ gₙ tends to f x. It is true however if the convergence of Fₙ to f is uniform. In this paragraph, we prove variations around this statement.

theorem tendsto_comp_of_locally_uniform_limit_within {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : ContinuousWithinAt f s x) (hg : Filter.Tendsto g p (nhdsWithin x s)) (hunif : ∀ u ∈ uniformity β, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ converges locally uniformly on a neighborhood of x within a set s to a function f which is continuous at x within s, and gₙ tends to x within s, then Fₙ (gₙ) tends to f x.

theorem tendsto_comp_of_locally_uniform_limit {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) (hunif : ∀ u ∈ uniformity β, ∃ t ∈ nhds x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ converges locally uniformly on a neighborhood of x to a function f which is continuous at x, and gₙ tends to x, then Fₙ (gₙ) tends to f x.

theorem TendstoLocallyUniformlyOn.tendsto_comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : TendstoLocallyUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hx : x ∈ s) (hg : Filter.Tendsto g p (nhdsWithin x s)) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends locally uniformly to f on a set s, and gₙ tends to x within s, then Fₙ gₙ tends to f x if f is continuous at x within s and x ∈ s.

theorem TendstoUniformlyOn.tendsto_comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : TendstoUniformlyOn F f p s) (hf : ContinuousWithinAt f s x) (hg : Filter.Tendsto g p (nhdsWithin x s)) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends uniformly to f on a set s, and gₙ tends to x within s, then Fₙ gₙ tends to f x if f is continuous at x within s.

theorem TendstoLocallyUniformly.tendsto_comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : TendstoLocallyUniformly F f p) (hf : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends locally uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.

theorem TendstoUniformly.tendsto_comp {α : Type u} {β : Type v} {ι : Type x} [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} [TopologicalSpace α] (h : TendstoUniformly F f p) (hf : ContinuousAt f x) (hg : Filter.Tendsto g p (nhds x)) : Filter.Tendsto (fun (n : ι) => F n (g n)) p (nhds (f x))

If Fₙ tends uniformly to f, and gₙ tends to x, then Fₙ gₙ tends to f x.