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
theorem
compact_space_uniformity
{α : Type u_1}
[uniform_space α]
[compact_space α]
[separated_space α] :
theorem
unique_uniformity_of_compact_t2
{α : Type u_1}
[t : topological_space α]
[compact_space α]
[t2_space α]
{u u' : uniform_space α}
(h : uniform_space.to_topological_space = t)
(h' : uniform_space.to_topological_space = t) :
u = u'
def
uniform_space_of_compact_t2
{α : Type (max (max u_1 u_2 u_3) u_2)}
[topological_space α]
[compact_space α]
[t2_space α] :
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 : α), 𝓝 (x, x), refl := _, symm := _, comp := _}, is_open_uniformity := _}
Heine-Cantor theorem
theorem
compact_space.uniform_continuous_of_continuous
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
[compact_space α]
[separated_space α]
{f : α → β}
(h : continuous f) :
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)
(hs' : is_separated s)
(hf : continuous_on f s) :
Heine-Cantor: a continuous function on a compact separated set of a uniform space is uniformly continuous.
theorem
is_compact.uniform_continuous_on_of_continuous
{α : Type u_1}
{β : Type u_2}
[uniform_space α]
[uniform_space β]
[separated_space α]
{s : set α}
{f : α → β}
(hs : is_compact s)
(hf : continuous_on f s) :
Heine-Cantor: a continuous function on a compact set of a separated uniform space is uniformly continuous.