of_surjective_continuous — 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\\; (Surjective f)\\rightarrow Continuous f \\rightarrow IsQuotientMap f.$$$

Lean4

/-- A continuous surjective map from a compact space to a Hausdorff space is a quotient map. -/
theorem of_surjective_continuous [CompactSpace X] [T2Space Y] {f : X → Y} (hsurj : Surjective f)
    (hcont : Continuous f) : IsQuotientMap f :=
  hcont.isClosedMap.isQuotientMap hcont hsurj

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