continuous_boolIndicator_iff_isClopen

English

For any subset U of X, U.boolIndicator is continuous if and only if U is clopen.

Русский

Для подмножества U пространства X функция-индикатор U.boolIndicator непрерывна тогда и только тогда, когда U клиopen.

LaTeX

$$$$ \text{Continuous}(U.boolIndicator) \;\Longleftrightarrow\; \operatorname{IsClopen}(U) $$$$

Lean4

theorem continuous_boolIndicator_iff_isClopen (U : Set X) : Continuous U.boolIndicator ↔ IsClopen U := by
  rw [continuous_bool_rng true, preimage_boolIndicator_true]

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