# Uniform approximation #

In this file, 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`.

## Implementation notes #

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

source
theorem continuousWithinAt_of_locally_uniform_approx_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} {s : Set α} {x : α} (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.

source
theorem continuousAt_of_locally_uniform_approx_of_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} {x : α} (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.

source
theorem continuousOn_of_locally_uniform_approx_of_continuousWithinAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} {s : Set α} (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.

source
theorem continuousOn_of_uniform_approx_of_continuousOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} {s : Set α} (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.

source
theorem continuous_of_locally_uniform_approx_of_continuousAt {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} (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.

source
theorem continuous_of_uniform_approx_of_continuous {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [UniformSpace β] {f : α → β} (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.

source
theorem TendstoLocallyUniformlyOn.continuousOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (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.

source
theorem TendstoUniformlyOn.continuousOn {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} (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.

source
theorem TendstoLocallyUniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (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.

source
theorem TendstoUniformly.continuous {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {p : Filter ι} (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.

source
theorem tendsto_comp_of_locally_uniform_limit_within {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} (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`.

source
theorem tendsto_comp_of_locally_uniform_limit {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} (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`.

source
theorem TendstoLocallyUniformlyOn.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} (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`.

source
theorem TendstoUniformlyOn.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {x : α} {p : Filter ι} {g : ι → α} (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`.

source
theorem TendstoLocallyUniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} (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`.

source
theorem TendstoUniformly.tendsto_comp {α : Type u_1} {β : Type u_2} {ι : Type u_3} [TopologicalSpace α] [UniformSpace β] {F : ι → α → β} {f : α → β} {x : α} {p : Filter ι} {g : ι → α} (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`.