Compact separated uniform spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main statements #

compact_space_uniformity: On a 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 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 spaces #

source

theorem nhds_set_diagonal_eq_uniformity {α : Type u_1} [uniform_space α] [compact_space α] :

nhds_set (set.diagonal α) = uniformity α

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

source

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.

source

theorem unique_uniformity_of_compact {γ : Type u_3} [t : topological_space γ] [compact_space γ] {u u' : uniform_space γ} (h : uniform_space.to_topological_space = t) (h' : uniform_space.to_topological_space = t) :

u = u'

source

def uniform_space_of_compact_t2 {γ : Type u_3} [topological_space γ] [compact_space γ] [t2_space γ] :

uniform_space γ

The unique uniform structure inducing a given compact topological structure.

Equations

uniform_space_of_compact_t2 = {to_topological_space := _inst_3, to_core := {uniformity := nhds_set (set.diagonal γ), refl := _, symm := _, comp := _}, is_open_uniformity := _}

Heine-Cantor theorem #

source

theorem compact_space.uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] [compact_space α] {f : α → β} (h : continuous f) :

uniform_continuous f

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

source

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) :

uniform_continuous_on f s

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

source

theorem is_compact.uniform_continuous_at_of_continuous_at {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {r : set (β × β)} {s : set α} (hs : is_compact s) (f : α → β) (hf : ∀ (a : α), a ∈ s → continuous_at f a) (hr : r ∈ uniformity β) :

{x : α × α | x.fst ∈ s → (f x.fst, f x.snd) ∈ r} ∈ uniformity α

If s is compact and f is continuous at all points of s, then f is "uniformly continuous at the set s", i.e. f x is close to f y whenever x ∈ s and y is close to x (even if y is not itself in s, so this is a stronger assertion than uniform_continuous_on s).

source

theorem continuous.uniform_continuous_of_tendsto_cocompact {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} {x : β} (h_cont : continuous f) (hx : filter.tendsto f (filter.cocompact α) (nhds x)) :

uniform_continuous f

source

theorem has_compact_mul_support.is_one_at_infty {α : Type u_1} {γ : Type u_3} [uniform_space α] {f : α → γ} [topological_space γ] [has_one γ] (h : has_compact_mul_support f) :

filter.tendsto f (filter.cocompact α) (nhds 1)

If f has compact multiplicative support, then f tends to 1 at infinity.

source

theorem has_compact_support.is_zero_at_infty {α : Type u_1} {γ : Type u_3} [uniform_space α] {f : α → γ} [topological_space γ] [has_zero γ] (h : has_compact_support f) :

filter.tendsto f (filter.cocompact α) (nhds 0)

If f has compact support, then f tends to zero at infinity.

source

theorem has_compact_support.uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} [has_zero β] (h1 : has_compact_support f) (h2 : continuous f) :

uniform_continuous f

source

theorem has_compact_mul_support.uniform_continuous_of_continuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {f : α → β} [has_one β] (h1 : has_compact_mul_support f) (h2 : continuous f) :

uniform_continuous f

source

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)) :

tendsto_uniformly f (f x) (nhds x)

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.

source

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 : α) :

tendsto_uniformly f (f x) (nhds x)

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

source

theorem compact_space.uniform_equicontinuous_of_equicontinuous {α : Type u_1} {β : Type u_2} [uniform_space α] [uniform_space β] {ι : Type u_3} {F : ι → β → α} [compact_space β] (h : equicontinuous F) :

uniform_equicontinuous F

An equicontinuous family of functions defined on a compact uniform space is automatically uniformly equicontinuous.