isQuotientMap_iff — Mathlib

English

A map is a quotient map if and only if it is surjective and a set is open in the codomain if and only if its preimage is open in the domain.

Русский

Отображение является факторизующим (коидом) тогда, когда оно сюръективно и открытость множества в кодоуме эквивалентна открытости его предобраза.

LaTeX

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

Lean4

theorem isQuotientMap_iff : IsQuotientMap f ↔ Surjective f ∧ ∀ s, IsOpen s ↔ IsOpen (f ⁻¹' s) :=
  (isQuotientMap_iff' _).trans <| and_congr Iff.rfl TopologicalSpace.ext_iff

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