# mathlibdocumentation

topology.uniform_space.uniform_convergence

# 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 at_top).

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

• tendsto_uniformly_on 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.
• tendsto_uniformly F f p: same notion with s = univ.
• tendsto_uniformly_on.continuous_on: a uniform limit on a set of functions which are continuous on this set is itself continuous on this set.
• tendsto_uniformly.continuous: a uniform limit of continuous functions is continuous.
• tendsto_uniformly_on.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.
• tendsto_uniformly.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 tendsto_locally_uniformly_on F f p s and tendsto_locally_uniformly 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 tendsto_uniformly_on_filter. 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 tendsto_uniformly_on_filter F f p (𝓝 x). Still, while this may be the "correct" definition (see tendsto_uniformly_on_iff_tendsto_uniformly_on_filter), it is somewhat unwieldy to work with in practice. Thus, we provide the more traditional definition in tendsto_uniformly_on.

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 tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} (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
theorem tendsto_uniformly_on_filter_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} :
p' filter.tendsto (λ (q : ι × α), (f q.snd, F q.fst q.snd)) (p.prod 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 tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} (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
• p s = ∀ (u : set × β)), u (∀ᶠ (n : ι) in p, ∀ (x : α), x s(f x, F n x) u)
theorem tendsto_uniformly_on_iff_tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} :
p s
theorem tendsto_uniformly_on_filter.tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} :
p s

Alias of the reverse direction of tendsto_uniformly_on_iff_tendsto_uniformly_on_filter.

theorem tendsto_uniformly_on.tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} :
p s

Alias of the forward direction of tendsto_uniformly_on_iff_tendsto_uniformly_on_filter.

theorem tendsto_uniformly_on_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {s : set α} :
p s filter.tendsto (λ (q : ι × α), (f q.snd, F q.fst q.snd)) (p.prod (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 tendsto_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} (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
• p = ∀ (u : set × β)), u (∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) u)
theorem tendsto_uniformly_iff_tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} :
p
theorem tendsto_uniformly.tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) :
theorem tendsto_uniformly_on_iff_tendsto_uniformly_comp_coe {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} :
p s tendsto_uniformly (λ (i : ι) (x : s), F i x) (f coe) p
theorem tendsto_uniformly_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} :
p filter.tendsto (λ (q : ι × α), (f q.snd, F q.fst q.snd)) (p.prod ) (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 tendsto_uniformly_on_filter.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {x : α} {p : filter ι} {p' : filter α} (h : p') (hx : p') :
filter.tendsto (λ (n : ι), F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem tendsto_uniformly_on.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p s) {x : α} (hx : x s) :
filter.tendsto (λ (n : ι), F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem tendsto_uniformly.tendsto_at {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) (x : α) :
filter.tendsto (λ (n : ι), F n x) p (nhds (f x))

Uniform converence implies pointwise convergence.

theorem tendsto_uniformly_on_univ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} :
p
theorem tendsto_uniformly_on_filter.mono_left {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} {p'' : filter ι} (h : p') (hp : p'' p) :
p'' p'
theorem tendsto_uniformly_on_filter.mono_right {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' p'' : filter α} (h : p') (hp : p'' p') :
p''
theorem tendsto_uniformly_on.mono {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {s' : set α} (h : p s) (h' : s' s) :
p s'
theorem tendsto_uniformly_on_filter.congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} {F' : ι → α → β} (hf : p') (hff' : ∀ᶠ (n : ι × α) in p.prod p', F n.fst n.snd = F' n.fst n.snd) :
p'
theorem tendsto_uniformly_on.congr {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {F' : ι → α → β} (hf : p s) (hff' : ∀ᶠ (n : ι) in p, set.eq_on (F n) (F' n) s) :
p s
@[protected]
theorem tendsto_uniformly.tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p) :
p s
theorem tendsto_uniformly_on_filter.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} (h : p') (g : γ → α) :
tendsto_uniformly_on_filter (λ (n : ι), F n g) (f g) p p')

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

theorem tendsto_uniformly_on.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p s) (g : γ → α) :
tendsto_uniformly_on (λ (n : ι), F n g) (f g) p (g ⁻¹' s)

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

theorem tendsto_uniformly.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) (g : γ → α) :
tendsto_uniformly (λ (n : ι), F n g) (f g) p

Composing on the right by a function preserves uniform convergence

theorem uniform_continuous.comp_tendsto_uniformly_on_filter {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} {g : β → γ} (hg : uniform_continuous g) (h : p') :
tendsto_uniformly_on_filter (λ (i : ι), g F i) (g f) p p'

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

theorem uniform_continuous.comp_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {g : β → γ} (hg : uniform_continuous g) (h : p s) :
tendsto_uniformly_on (λ (i : ι), g F i) (g f) p s

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

theorem uniform_continuous.comp_tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {g : β → γ} (hg : uniform_continuous g) (h : p) :
tendsto_uniformly (λ (i : ι), g F i) (g f) p

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

theorem tendsto_uniformly_on_filter.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} {ι' : Type u_3} {α' : Type u_5} {β' : Type u_6} [uniform_space β'] {F' : ι' → α' → β'} {f' : α' → β'} {q : filter ι'} {q' : filter α'} (h : p') (h' : q q') :
tendsto_uniformly_on_filter (λ (i : ι × ι'), prod.map (F i.fst) (F' i.snd)) (prod.map f f') (p.prod q) (p'.prod q')
theorem tendsto_uniformly_on.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {ι' : Type u_3} {α' : Type u_5} {β' : Type u_6} [uniform_space β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : filter ι'} {s' : set α'} (h : p s) (h' : f' p' s') :
tendsto_uniformly_on (λ (i : ι × ι'), prod.map (F i.fst) (F' i.snd)) (prod.map f f') (p.prod p') (s ×ˢ s')
theorem tendsto_uniformly.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {ι' : Type u_3} {α' : Type u_5} {β' : Type u_6} [uniform_space β'] {F' : ι' → α' → β'} {f' : α' → β'} {p' : filter ι'} (h : p) (h' : f' p') :
tendsto_uniformly (λ (i : ι × ι'), prod.map (F i.fst) (F' i.snd)) (prod.map f f') (p.prod p')
theorem tendsto_uniformly_on_filter.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} {ι' : Type u_3} {β' : Type u_5} [uniform_space β'] {F' : ι' → α → β'} {f' : α → β'} {q : filter ι'} (h : p') (h' : q p') :
tendsto_uniformly_on_filter (λ (i : ι × ι') (a : α), (F i.fst a, F' i.snd a)) (λ (a : α), (f a, f' a)) (p.prod q) p'
theorem tendsto_uniformly_on.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {ι' : Type u_3} {β' : Type u_5} [uniform_space β'] {F' : ι' → α → β'} {f' : α → β'} {p' : filter ι'} (h : p s) (h' : f' p' s) :
tendsto_uniformly_on (λ (i : ι × ι') (a : α), (F i.fst a, F' i.snd a)) (λ (a : α), (f a, f' a)) (p.prod p') s
theorem tendsto_uniformly.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {ι' : Type u_3} {β' : Type u_5} [uniform_space β'] {F' : ι' → α → β'} {f' : α → β'} {p' : filter ι'} (h : p) (h' : f' p') :
tendsto_uniformly (λ (i : ι × ι') (a : α), (F i.fst a, F' i.snd a)) (λ (a : α), (f a, f' a)) (p.prod p')
theorem tendsto_prod_filter_iff {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {p : filter ι} {p' : filter α} {c : β} :
(p.prod p') (nhds c) (λ (_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_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {c : β} :
(p.prod (filter.principal s)) (nhds c) (λ (_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_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {p : filter ι} {c : β} :
(p.prod ) (nhds c) (λ (_x : α), c) p

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

theorem tendsto_uniformly_on_empty {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} :
p

Uniform convergence on the empty set is vacuously true

theorem tendsto_uniformly_on_singleton_iff_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {x : α} {p : filter ι} :
p {x} filter.tendsto (λ (n : ι), F n x) p (nhds (f x))

Uniform convergence on a singleton is equivalent to regular convergence

theorem filter.tendsto.tendsto_uniformly_on_filter_const {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : filter ι} {g : ι → β} {b : β} (hg : (nhds b)) (p' : filter α) :
tendsto_uniformly_on_filter (λ (n : ι) (a : α), g n) (λ (a : α), b) p p'

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

theorem filter.tendsto.tendsto_uniformly_on_const {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : filter ι} {g : ι → β} {b : β} (hg : (nhds b)) (s : set α) :
tendsto_uniformly_on (λ (n : ι) (a : α), g n) (λ (a : α), b) p s

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

theorem uniform_continuous_on.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : α} {U : set α} (hU : U nhds x) {F : α → β → γ} (hF : (U ×ˢ set.univ)) :
(F x) (nhds x)
theorem uniform_continuous₂.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} (h : uniform_continuous₂ f) {x : α} :
(f x) (nhds x)
def uniform_cauchy_seq_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} (F : ι → α → β) (p : filter ι) (p' : filter α) :
Prop

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

Equations
def uniform_cauchy_seq_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} (F : ι → α → β) (p : filter ι) (s : set α) :
Prop

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

Equations
theorem uniform_cauchy_seq_on_iff_uniform_cauchy_seq_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} :
theorem uniform_cauchy_seq_on.uniform_cauchy_seq_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} (hF : s) :
theorem tendsto_uniformly_on_filter.uniform_cauchy_seq_on_filter {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} (hF : p') :

A sequence that converges uniformly is also uniformly Cauchy

theorem tendsto_uniformly_on.uniform_cauchy_seq_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (hF : p s) :

A sequence that converges uniformly is also uniformly Cauchy

theorem uniform_cauchy_seq_on_filter.tendsto_uniformly_on_filter_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} {p' : filter α} [p.ne_bot] (hF : p') (hF' : ∀ᶠ (x : α) in p', filter.tendsto (λ (n : ι), F n x) p (nhds (f x))) :
p'

A uniformly Cauchy sequence converges uniformly to its limit

theorem uniform_cauchy_seq_on.tendsto_uniformly_on_of_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} [p.ne_bot] (hF : s) (hF' : ∀ (x : α), x sfilter.tendsto (λ (n : ι), F n x) p (nhds (f x))) :
p s

A uniformly Cauchy sequence converges uniformly to its limit

theorem uniform_cauchy_seq_on_filter.mono_left {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {p : filter ι} {p' : filter α} {p'' : filter ι} (hf : p') (hp : p'' p) :
p'
theorem uniform_cauchy_seq_on_filter.mono_right {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {p : filter ι} {p' p'' : filter α} (hf : p') (hp : p'' p') :
p''
theorem uniform_cauchy_seq_on.mono {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {s' : set α} (hf : s) (hss' : s' s) :
s'
theorem uniform_cauchy_seq_on_filter.comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {p : filter ι} {p' : filter α} {γ : Type u_3} (hf : p') (g : γ → α) :
uniform_cauchy_seq_on_filter (λ (n : ι), F n g) p p')

Composing on the right by a function preserves uniform Cauchy sequences

theorem uniform_cauchy_seq_on.comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {γ : Type u_3} (hf : s) (g : γ → α) :
uniform_cauchy_seq_on (λ (n : ι), F n g) p (g ⁻¹' s)

Composing on the right by a function preserves uniform Cauchy sequences

theorem uniform_continuous.comp_uniform_cauchy_seq_on {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {g : β → γ} (hg : uniform_continuous g) (hf : s) :
uniform_cauchy_seq_on (λ (n : ι), g F n) p s

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

theorem uniform_cauchy_seq_on.prod_map {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {ι' : Type u_3} {α' : Type u_5} {β' : Type u_6} [uniform_space β'] {F' : ι' → α' → β'} {p' : filter ι'} {s' : set α'} (h : s) (h' : s') :
uniform_cauchy_seq_on (λ (i : ι × ι'), prod.map (F i.fst) (F' i.snd)) (p.prod p') (s ×ˢ s')
theorem uniform_cauchy_seq_on.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {ι' : Type u_3} {β' : Type u_5} [uniform_space β'] {F' : ι' → α → β'} {p' : filter ι'} (h : s) (h' : s) :
uniform_cauchy_seq_on (λ (i : ι × ι') (a : α), (F i.fst a, F' i.snd a)) (p.prod p') s
theorem uniform_cauchy_seq_on.prod' {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {s : set α} {p : filter ι} {β' : Type u_3} [uniform_space β'] {F' : ι → α → β'} (h : s) (h' : s) :
uniform_cauchy_seq_on (λ (i : ι) (a : α), (F i a, F' i a)) p s
theorem tendsto_uniformly_on_of_seq_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {l : filter ι} (h : ∀ (u : → ι), tendsto_uniformly_on (λ (n : ), F (u n)) f filter.at_top s) :
l s
theorem tendsto_uniformly_on.seq_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {l : filter ι} (h : l s) (u : → ι) (hu : l) :
tendsto_uniformly_on (λ (n : ), F (u n)) f filter.at_top s
theorem tendsto_uniformly_on_iff_seq_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {l : filter ι}  :
l s ∀ (u : → ι), tendsto_uniformly_on (λ (n : ), F (u n)) f filter.at_top s
theorem tendsto_uniformly_iff_seq_tendsto_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {l : filter ι}  :
l ∀ (u : → ι), tendsto_uniformly (λ (n : ), F (u n)) f filter.at_top
def tendsto_locally_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} (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
• s = ∀ (u : set × β)), u ∀ (x : α), x s(∃ (t : set α) (H : t s), ∀ᶠ (n : ι) in p, ∀ (y : α), y t(f y, F n y) u)
def tendsto_locally_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} (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
• = ∀ (u : set × β)), u ∀ (x : α), ∃ (t : set α) (H : t nhds x), ∀ᶠ (n : ι) in p, ∀ (y : α), y t(f y, F n y) u
theorem tendsto_locally_uniformly_on_iff_tendsto_locally_uniformly_comp_coe {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι}  :
s tendsto_locally_uniformly (λ (i : ι) (x : s), F i x) (f coe) p
theorem tendsto_locally_uniformly_iff_forall_tendsto {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι}  :
∀ (x : α), filter.tendsto (λ (y : ι × α), (f y.snd, F y.fst y.snd)) (p.prod (nhds x)) (uniformity β)
@[protected]
theorem tendsto_uniformly_on.tendsto_locally_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p s) :
s
@[protected]
theorem tendsto_uniformly.tendsto_locally_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) :
theorem tendsto_locally_uniformly_on.mono {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s s' : set α} {p : filter ι} (h : s) (h' : s' s) :
s'
theorem tendsto_locally_uniformly_on_univ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι}  :
@[protected]
theorem tendsto_locally_uniformly.tendsto_locally_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p) :
s
theorem tendsto_locally_uniformly_iff_tendsto_uniformly_of_compact_space {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι}  :
p

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

theorem tendsto_locally_uniformly_on_iff_tendsto_uniformly_on_of_compact {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (hs : is_compact s) :
s p s

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

theorem tendsto_locally_uniformly_on.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} {t : set γ} (h : s) (g : γ → α) (hg : t s) (cg : t) :
tendsto_locally_uniformly_on (λ (n : ι), F n g) (f g) p t
theorem tendsto_locally_uniformly.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) (g : γ → α) (cg : continuous g) :
tendsto_locally_uniformly (λ (n : ι), F n g) (f g) p

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

theorem continuous_within_at_of_locally_uniform_approx_of_continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} {x : α} (hx : x s) (L : ∀ (u : set × β)), u (∃ (t : set α) (H : t s) (F : α → β), x ∀ (y : α), y t(f y, F y) u)) :
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 continuous_at_of_locally_uniform_approx_of_continuous_at {α : Type u_1} {β : Type u_2} {f : α → β} {x : α} (L : ∀ (u : set × β)), u (∃ (t : set α) (H : t nhds x) (F : α → β), ∀ (y : α), y t(f y, F y) u)) :

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

theorem continuous_on_of_locally_uniform_approx_of_continuous_within_at {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (L : ∀ (x : α), x s∀ (u : set × β)), u (∃ (t : set α) (H : t s) (F : α → β), x ∀ (y : α), y t(f y, F y) u)) :

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

theorem continuous_on_of_uniform_approx_of_continuous_on {α : Type u_1} {β : Type u_2} {f : α → β} {s : set α} (L : ∀ (u : set × β)), u (∃ (F : α → β), ∀ (y : α), y s(f y, F y) u)) :

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_continuous_at {α : Type u_1} {β : Type u_2} {f : α → β} (L : ∀ (x : α) (u : set × β)), u (∃ (t : set α) (H : t nhds x) (F : α → β), ∀ (y : α), y t(f y, F y) u)) :

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

theorem continuous_of_uniform_approx_of_continuous {α : Type u_1} {β : Type u_2} {f : α → β} (L : ∀ (u : set × β)), u (∃ (F : α → β), ∀ (y : α), (f y, F y) u)) :

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.

@[protected]
theorem tendsto_locally_uniformly_on.continuous_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : s) (hc : ∀ᶠ (n : ι) in p, continuous_on (F n) s) [p.ne_bot] :

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

@[protected]
theorem tendsto_uniformly_on.continuous_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {p : filter ι} (h : p s) (hc : ∀ᶠ (n : ι) in p, continuous_on (F n) s) [p.ne_bot] :

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

@[protected]
theorem tendsto_locally_uniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) (hc : ∀ᶠ (n : ι) in p, continuous (F n)) [p.ne_bot] :

A locally uniform limit of continuous functions is continuous.

@[protected]
theorem tendsto_uniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} (h : p) (hc : ∀ᶠ (n : ι) in p, continuous (F n)) [p.ne_bot] :

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_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {x : α} {p : filter ι} {g : ι → α} (h : x) (hg : s)) (hunif : ∀ (u : set × β)), u (∃ (t : set α) (H : t s), ∀ᶠ (n : ι) in p, ∀ (y : α), y t(f y, F n y) u)) :
filter.tendsto (λ (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_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {x : α} {p : filter ι} {g : ι → α} (h : x) (hg : (nhds x)) (hunif : ∀ (u : set × β)), u (∃ (t : set α) (H : t nhds x), ∀ᶠ (n : ι) in p, ∀ (y : α), y t(f y, F n y) u)) :
filter.tendsto (λ (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 tendsto_locally_uniformly_on.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {x : α} {p : filter ι} {g : ι → α} (h : s) (hf : x) (hx : x s) (hg : s)) :
filter.tendsto (λ (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 tendsto_uniformly_on.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {s : set α} {x : α} {p : filter ι} {g : ι → α} (h : p s) (hf : x) (hg : s)) :
filter.tendsto (λ (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 tendsto_locally_uniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {x : α} {p : filter ι} {g : ι → α} (h : p) (hf : x) (hg : (nhds x)) :
filter.tendsto (λ (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 tendsto_uniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {x : α} {p : filter ι} {g : ι → α} (h : p) (hf : x) (hg : (nhds x)) :
filter.tendsto (λ (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.