isClosedMap — Mathlib

English

A continuous map from a compact space to a Hausdorff space is a closed map.

Русский

Непрерывное отображение из компактного пространства в Хаусдорфовоe пространство — замкнутое отображение.

LaTeX

$$$[CompactSpace X][T2Space Y]\\; f:X\\to Y\\Rightarrow IsClosedMap f.$$$

Lean4

/-- A continuous map from a compact space to a Hausdorff space is a closed map. -/
protected theorem isClosedMap [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) : IsClosedMap f :=
  fun _s hs => (hs.isCompact.image h).isClosed

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