isQuotientMap — Mathlib

English

A closed map with surjectivity and continuity yields a quotient map.

Русский

Замкнутое отображение с сюръективностью и непрерывностью порождает факторное отображение.

LaTeX

$$$IsClosedMap f \\land Continuous f \\land Surjective f \\Rightarrow IsQuotientMap f$$$

Lean4

theorem isQuotientMap (hcl : IsClosedMap f) (hcont : Continuous f) (hsurj : Surjective f) : IsQuotientMap f :=
  isQuotientMap_iff_isClosed.2
    ⟨hsurj, fun s => ⟨fun hs => hs.preimage hcont, fun hs => hsurj.image_preimage s ▸ hcl _ hs⟩⟩

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