Compact separated uniform spaces #
Main statements #
compact_space_uniformity
: On a separated compact uniform space, the topology determines the uniform structure, entourages are exactly the neighborhoods of the diagonal.uniform_space_of_compact_t2
: every compact T2 topological structure is induced by a uniform structure. This uniform structure is described in the previous item.- Heine-Cantor theorem: continuous functions on compact separated uniform spaces with values in
uniform spaces are automatically uniformly continuous. There are several variations, the main one
is
compact_space.uniform_continuous_of_continuous
.
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 separated spaces #
On a separated 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 Hausdorff topological structure.
Equations
- uniform_space_of_compact_t2 = {to_topological_space := _inst_3, to_core := {uniformity := ⨆ (x : γ), nhds (x, x), refl := _, symm := _, comp := _}, is_open_uniformity := _}
Heine-Cantor theorem #
Heine-Cantor: a continuous function on a compact separated uniform space is uniformly continuous.
Heine-Cantor: a continuous function on a compact separated set of a uniform space is uniformly continuous.
Heine-Cantor: a continuous function on a compact set of a separated uniform space is uniformly continuous.
A family of functions α → β → γ
tends uniformly to its value at x
if α
is locally compact,
β
is compact and separated and f
is continuous on U × (univ : set β)
for some separated
neighborhood U
of x
.
A continuous family of functions α → β → γ
tends uniformly to its value at x
if α
is
locally compact and β
is compact and separated.