continuousOn_boolIndicator_iff_isClopen

English

For any s and U ⊆ X, continuousOn of U.boolIndicator on s is equivalent to IsClopen of the preimage of U under the inclusion map into X.

Русский

Для любых s и U ⊆ X непрерывность на s булева индикатора эквивалентна тому, что предобраз U по включению в X является клиopen.

LaTeX

$$$$ \text{ContinuousOn}(U.boolIndicator\; s) \;\Longleftrightarrow\; \operatorname{IsClopen}\left((\uparrow):s\to X)^{-1}' U\right) $$$$

Lean4

theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :
    ContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U) :=
  by
  rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]
  rfl

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