Compact separated uniform spaces

Main statements

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

• uniformSpace_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 CompactSpace.uniformContinuous_of_continuous.

Implementation notes

The construction uniformSpace_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

theorem nhdsSet_diagonal_eq_uniformity {α : Type u_1} [UniformSpace α] [CompactSpace α] : nhdsSet (Set.diagonal α) = uniformity α

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

theorem compactSpace_uniformity {α : Type u_1} [UniformSpace α] [CompactSpace α] : uniformity α = ⨆ (x : α), nhds (x, x)

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

theorem unique_uniformity_of_compact {γ : Type u_3} [t : TopologicalSpace γ] [CompactSpace γ] {u : UniformSpace γ} {u' : UniformSpace γ} (h : UniformSpace.toTopologicalSpace = t) (h' : UniformSpace.toTopologicalSpace = t) : u = u'

def uniformSpaceOfCompactT2 {γ : Type u_3} [TopologicalSpace γ] [CompactSpace γ] [T2Space γ] : UniformSpace γ

The unique uniform structure inducing a given compact topological structure.

Equations

• One or more equations did not get rendered due to their size.

### Heine-Cantor theorem

theorem CompactSpace.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] [CompactSpace α] {f : α → β} (h : Continuous f) : UniformContinuous f

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

theorem IsCompact.uniformContinuousOn_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {s : Set α} {f : α → β} (hs : IsCompact s) (hf : ContinuousOn f s) : UniformContinuousOn f s

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

theorem IsCompact.uniformContinuousAt_of_continuousAt {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {r : Set (β × β)} {s : Set α} (hs : IsCompact s) (f : α → β) (hf : ∀ a ∈ s, ContinuousAt f a) (hr : r ∈ uniformity β) : {x : α × α | x.1 ∈ s → (f x.1, f x.2) ∈ 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 UniformContinuousOn s).

theorem Continuous.uniformContinuous_of_tendsto_cocompact {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} {x : β} (h_cont : Continuous f) (hx : Filter.Tendsto f (Filter.cocompact α) (nhds x)) : UniformContinuous f

theorem HasCompactSupport.is_zero_at_infty {α : Type u_1} {γ : Type u_3} [UniformSpace α] {f : α → γ} [TopologicalSpace γ] [Zero γ] (h : HasCompactSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 0)

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

theorem HasCompactMulSupport.is_one_at_infty {α : Type u_1} {γ : Type u_3} [UniformSpace α] {f : α → γ} [TopologicalSpace γ] [One γ] (h : HasCompactMulSupport f) : Filter.Tendsto f (Filter.cocompact α) (nhds 1)

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

theorem HasCompactSupport.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} [Zero β] (h1 : HasCompactSupport f) (h2 : Continuous f) : UniformContinuous f

theorem HasCompactMulSupport.uniformContinuous_of_continuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {f : α → β} [One β] (h1 : HasCompactMulSupport f) (h2 : Continuous f) : UniformContinuous f

theorem ContinuousOn.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace α] [UniformSpace β] [LocallyCompactSpace α] [CompactSpace β] [UniformSpace γ] {f : α → β → γ} {x : α} {U : Set α} (hxU : U ∈ nhds x) (h : ContinuousOn (↿f) (U ×ˢ Set.univ)) : TendstoUniformly 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.

theorem Continuous.tendstoUniformly {α : Type u_1} {β : Type u_2} {γ : Type u_3} [UniformSpace α] [UniformSpace β] [WeaklyLocallyCompactSpace α] [CompactSpace β] [UniformSpace γ] (f : α → β → γ) (h : Continuous ↿f) (x : α) : TendstoUniformly f (f x) (nhds x)

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

theorem IsCompact.mem_uniformity_of_prod {α : Type u_4} {β : Type u_5} {E : Type u_6} [TopologicalSpace α] [TopologicalSpace β] [UniformSpace E] {f : α → β → E} {s : Set α} {k : Set β} {q : α} {u : Set (E × E)} (hk : IsCompact k) (hf : ContinuousOn (Function.uncurry f) (s ×ˢ k)) (hq : q ∈ s) (hu : u ∈ uniformity E) : ∃ v ∈ nhdsWithin q s, ∀ p ∈ v, ∀ x ∈ k, (f p x, f q x) ∈ u

In a product space α × β, assume that a function f is continuous on s × k where k is compact. Then, along the fiber above any q ∈ s, f is transversely uniformly continuous, i.e., if p ∈ s is close enough to q, then f p x is uniformly close to f q x for all x ∈ k.

theorem CompactSpace.uniformEquicontinuous_of_equicontinuous {α : Type u_1} {β : Type u_2} [UniformSpace α] [UniformSpace β] {ι : Type u_4} {F : ι → β → α} [CompactSpace β] (h : Equicontinuous F) : UniformEquicontinuous F

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