isClopen_preimage — Mathlib

English

If f is a quotient map, then a set s is clopen iff its preimage under f is clopen.

Русский

Если f есть факторизация (квазиобраз), тогда множество s открыто и замкнуто тогда предобраз под f также.

LaTeX

$$$$ \operatorname{IsClopen}\left( f^{-1}(s) \right) \;\Longleftrightarrow\; \operatorname{IsClopen}(s) $$$$

Lean4

protected theorem isClopen_preimage {f : X → Y} (hf : IsQuotientMap f) {s : Set Y} : IsClopen (f ⁻¹' s) ↔ IsClopen s :=
  and_congr hf.isClosed_preimage hf.isOpen_preimage

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