iff_isOpenMap_isQuotientMap — Mathlib

English

An open quotient map is equivalent to being open and a quotient map together.

Русский

Открытое факторное отображение эквивалентно сочетанию открытости и факторности.

LaTeX

$$$\mathrm{IsOpenQuotientMap}(f) \iff \big( \mathrm{IsOpenMap}(f) \land \mathrm{IsQuotientMap}(f) \big)$$$

Lean4

theorem iff_isOpenMap_isQuotientMap : IsOpenQuotientMap f ↔ IsOpenMap f ∧ IsQuotientMap f :=
  ⟨fun h ↦ ⟨h.isOpenMap, h.isQuotientMap⟩, fun ⟨ho, hq⟩ ↦ ⟨hq.surjective, hq.continuous, ho⟩⟩

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