isQuotientMap_iff_isClosed — Mathlib

English

A quotient map f is characterized by surjectivity and the property that a set is closed in Y iff its preimage is closed in X.

Русский

Картографическое отображение-факторизация характеризуется сюръективностью и тем, что множество закрыто в Y тогда и только тогда, когда его прообраз закрыт в X.

LaTeX

$$$\mathrm{IsQuotientMap}(f) \iff \Big( \mathrm{Surjective}(f) \land \forall s, \mathrm{IsClosed}(s) \leftrightarrow \mathrm{IsClosed}(f^{-1}(s)) \Big)$$$

Lean4

theorem isQuotientMap_iff_isClosed : IsQuotientMap f ↔ Surjective f ∧ ∀ s : Set Y, IsClosed s ↔ IsClosed (f ⁻¹' s) :=
  isQuotientMap_iff.trans <|
    Iff.rfl.and <| compl_surjective.forall.trans <| by simp only [isOpen_compl_iff, preimage_compl]

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