isOpen_preimage — Mathlib

English

Let f be a quotient map. Then a subset s of the codomain Y is open if and only if its preimage under f is open in X.

Русский

Пусть f является факторизующим отображением. Тогда множество s ⊆ Y открыто тогда и только тогда, когда его прообраз f^{-1}(s) открыт в X.

LaTeX

$$$$IsQuotientMap(f) \\rightarrow \\forall s \\subseteq Y, \\ Open(f^{-1}(s)) \\iff Open(s)$$$$

Lean4

protected theorem isOpen_preimage (hf : IsQuotientMap f) {s : Set Y} : IsOpen (f ⁻¹' s) ↔ IsOpen s :=
  ((isQuotientMap_iff.1 hf).2 s).symm

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