isClosedMap — Mathlib

English

Any continuous map between compact Hausdorff spaces is a closed map.

Русский

Любое непрерывное отображение между компактно-хаусдорфовыми пространствами является замкнутым отображением.

LaTeX

$$$\mathrm{IsClosedMap}(f)$ for $f:X\to Y$ in CompHausLike P$$

Lean4

/-- Any continuous function on compact Hausdorff spaces is a closed map. -/
theorem isClosedMap {X Y : CompHausLike.{u} P} (f : X ⟶ Y) : IsClosedMap f := fun _ hC =>
  (hC.isCompact.image f.hom.continuous).isClosed

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