mathlib documentation

topology.uniform_space.uniform_convergence_topology

Topology and uniform structure of uniform convergence #

This files endows α → β with the topologies / uniform structures of

Usual examples of the second construction include :

Main definitions #

Main statements #

Implementation details #

We do not declare these structures as instances, since they would conflict with Pi.uniform_space.

TODO #

References #

Tags #

uniform convergence

@[protected]
def uniform_convergence.gen (α : Type u_1) (β : Type u_2) (V : set × β)) :
set ((α → β) × (α → β))

Basis sets for the uniformity of uniform convergence

Equations
@[protected]
theorem uniform_convergence.is_basis_gen (α : Type u_1) (β : Type u_2) [uniform_space β] :
filter.is_basis (λ (V : set × β)), V uniformity β) (uniform_convergence.gen α β)
@[protected]
def uniform_convergence.uniformity_basis (α : Type u_1) (β : Type u_2) [uniform_space β] :
filter_basis ((α → β) × (α → β))

Filter basis for the uniformity of uniform convergence

Equations
@[protected]
def uniform_convergence.uniform_core (α : Type u_1) (β : Type u_2) [uniform_space β] :
uniform_space.core (α → β)

Core of the uniform structure of uniform convergence

Equations
@[protected]
def uniform_convergence.uniform_space (α : Type u_1) (β : Type u_2) [uniform_space β] :
uniform_space (α → β)

Uniform structure of uniform convergence

Equations
@[protected]
theorem uniform_convergence.has_basis_uniformity (α : Type u_1) (β : Type u_2) [uniform_space β] :
(uniformity (α → β)).has_basis (λ (V : set × β)), V uniformity β) (uniform_convergence.gen α β)
@[protected]
def uniform_convergence.topological_space (α : Type u_1) (β : Type u_2) [uniform_space β] :
topological_space (α → β)

Topology of uniform convergence

Equations
@[protected]
theorem uniform_convergence.has_basis_nhds (α : Type u_1) (β : Type u_2) {f : α → β} [uniform_space β] :
(nhds f).has_basis (λ (V : set × β)), V uniformity β) (λ (V : set × β)), {g : α → β | (g, f) uniform_convergence.gen α β V})
theorem uniform_convergence.uniform_continuous_eval {α : Type u_1} (β : Type u_2) [uniform_space β] (x : α) :
theorem uniform_convergence.t2_space {α : Type u_1} {β : Type u_2} [uniform_space β] [t2_space β] :
t2_space (α → β)
@[protected]
theorem uniform_convergence.le_Pi {α : Type u_1} {β : Type u_2} [uniform_space β] :
@[protected]
theorem uniform_convergence.tendsto_iff_tendsto_uniformly {α : Type u_1} {β : Type u_2} {ι : Type u_4} {F : ι → α → β} {f : α → β} {p : filter ι} [uniform_space β] :
@[protected]
def uniform_convergence_on.uniform_space (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) :
uniform_space (α → β)

Uniform structure of uniform convergence on the sets of 𝔖.

Equations
@[protected]
def uniform_convergence_on.topological_space (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) :
topological_space (α → β)

Topology of uniform convergence on the sets of 𝔖.

Equations
@[protected]
theorem uniform_convergence_on.topological_space_eq (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) :
@[protected]
theorem uniform_convergence_on.uniform_continuous_restrict (α : Type u_1) (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) {s : set α} (h : s 𝔖) :
@[protected]
theorem uniform_convergence_on.uniform_continuous_eval_of_mem {α : Type u_1} (β : Type u_2) [uniform_space β] (𝔖 : set (set α)) {s : set α} {x : α} (hxs : x s) (hs : s 𝔖) :
theorem uniform_convergence_on.t2_space_of_covering {α : Type u_1} {β : Type u_2} [uniform_space β] (𝔖 : set (set α)) [t2_space β] (h : ⋃₀ 𝔖 = set.univ) :
t2_space (α → β)
@[protected]
theorem uniform_convergence_on.le_Pi_of_covering {α : Type u_1} {β : Type u_2} [uniform_space β] (𝔖 : set (set α)) (h : ⋃₀ 𝔖 = set.univ) :
@[protected]
theorem uniform_convergence_on.tendsto_iff_tendsto_uniformly_on {α : Type u_1} {β : Type u_2} {ι : Type u_4} [uniform_space β] (𝔖 : set (set α)) {F : ι → α → β} {f : α → β} {p : filter ι} :
filter.tendsto F p (nhds f) ∀ (s : set α), s 𝔖tendsto_uniformly_on F f p s