image_closure_of_isCompact — Mathlib

English

A continuous surjective map from a compact space to a Hausdorff space is a quotient map.

Русский

Непрерывное сюръективное отображение из компактного пространства в Хаусдорфовоe является факторной картой (квартированным отображением).

LaTeX

$$$[CompactSpace X][T2Space Y]\\; f:X\\to Y\\;\\text{ surjective } f \\land Continuous f \\Rightarrow IsQuotientMap f.$$$

Lean4

theorem image_closure_of_isCompact [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : X → Y}
    (hf : ContinuousOn f (closure s)) : f '' closure s = closure (f '' s) :=
  Subset.antisymm hf.image_closure <| closure_minimal (image_mono subset_closure) (hs.image_of_continuousOn hf).isClosed

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