of_isOpenMap_isQuotientMap — Mathlib

English

If f is open and a quotient map, then it is an open quotient map.

Русский

Если f открыто и является факторным отображением, то оно открытое факторное отображение.

LaTeX

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

Lean4

theorem of_isOpenMap_isQuotientMap (ho : IsOpenMap f) (hq : IsQuotientMap f) : IsOpenQuotientMap f :=
  iff_isOpenMap_isQuotientMap.2 ⟨ho, hq⟩

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