isClopen_preimage — Mathlib

English

For every subset A of the quotient, the preimage π^{-1}(A) is clopen in X.

Русский

Для каждого множества A подпространства факторпространства прообраз π^{-1}(A) является открытым и закрытым в X.

LaTeX

$$$ \\forall A \\subseteq X/\\sim,\\ IsClopen(\\pi^{-1}(A)) $$$

Lean4

theorem isClopen_preimage (A : Set S) : IsClopen (S.proj ⁻¹' A) :=
  (isClopen_discrete A).preimage S.proj_continuous

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