mathlib documentation

topology.uniform_space.compact_separated

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 separated spaces

theorem compact_space_uniformity {α : Type u_1} [uniform_space α] [compact_space α] [separated_space α] :
𝓤 α = ⨆ (x : α), 𝓝 (x, x)

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

 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 : α → β} :

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 : α → β} :

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 : α → β} :

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