continuous_bool_rng — Mathlib

English

A function from a topological space X to a discrete Bool space is continuous if and only if the preimage of the singleton {b} is clopen, for b ∈ Bool.

Русский

Отображение из X в дискретное булево множество непрерывно тогда и только тогда, когда прообраз любого одинокого множества {b} является одновременно открытым и замкнутым.

LaTeX

$$$$ \\text{Continuous}(f) \\iff \\text{IsClopen}(f^{-1}({b})). $$$$

Lean4

theorem continuous_bool_rng [TopologicalSpace X] {f : X → Bool} (b : Bool) : Continuous f ↔ IsClopen (f ⁻¹' { b }) := by
  rw [continuous_discrete_rng, Bool.forall_bool' b, IsClopen, ← isOpen_compl_iff, ← preimage_compl,
    Bool.compl_singleton, and_comm]

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