mathlib documentation

topology.uniform_space.compact

Compact separated uniform spaces #

Main statements #

Implementation notes #

The construction uniform_space_of_compact_t2 is not declared as an instance, as it would badly loop.

tags #

uniform space, uniform continuity, compact space

Uniformity on compact spaces #

On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

theorem compact_space_uniformity {α : Type u_1} [uniform_space α] [compact_space α] :
uniformity α = (x : α), nhds (x, x)

On a compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.

The unique uniform structure inducing a given compact topological structure.

Equations

Heine-Cantor theorem #

Heine-Cantor: a continuous function on a compact separated uniform space is uniformly continuous.

theorem is_compact.uniform_continuous_on_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {s : set α} {f : α β} (hs : is_compact s) (hf : continuous_on f s) :

Heine-Cantor: a continuous function on a compact set of a uniform space is uniformly continuous.

theorem continuous_on.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [locally_compact_space α] [compact_space β] [uniform_space γ] {f : α β γ} {x : α} {U : set α} (hxU : U nhds x) (h : continuous_on f (U ×ˢ set.univ)) :

A family of functions α → β → γ tends uniformly to its value at x if α is locally compact, β is compact and f is continuous on U × (univ : set β) for some neighborhood U of x.

theorem continuous.tendsto_uniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [uniform_space α] [uniform_space β] [locally_compact_space α] [compact_space β] [uniform_space γ] (f : α β γ) (h : continuous f) (x : α) :

A continuous family of functions α → β → γ tends uniformly to its value at x if α is locally compact and β is compact.