uniformContinuous_of_continuous — Mathlib

English

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

Русский

Гейне–Канторо: непрерывная функция на компактном равномерном пространстве является равномерно непрерывной.

LaTeX

$$\\text{If } α \\text{ is compact and } f: α \\to β \\text{ is continuous, then } f \\text{ is uniformly continuous}.$$

Lean4

/-- Heine-Cantor: a continuous function on a compact uniform space is uniformly
continuous. -/
theorem uniformContinuous_of_continuous [CompactSpace α] {f : α → β} (h : Continuous f) : UniformContinuous f :=
  calc
    map (Prod.map f f) (𝓤 α) = map (Prod.map f f) (𝓝ˢ (diagonal α)) := by rw [nhdsSet_diagonal_eq_uniformity]
    _ ≤ 𝓝ˢ (diagonal β) := ((h.prodMap h).tendsto_nhdsSet mapsTo_prodMap_diagonal)
    _ ≤ 𝓤 β := nhdsSet_diagonal_le_uniformity

Похожие утверждения