of_discrete — Mathlib

English

TotallySeparatedSpace α implies TotallyDisconnectedSpace α.

Русский

TotallySeparatedSpace α влечет TotallyDisconnectedSpace α.

LaTeX

$$TotallySeparatedSpace(α) \Rightarrow TotallyDisconnectedSpace(α)$$

Lean4

instance (priority := 100) of_discrete (α : Type*) [TopologicalSpace α] [DiscreteTopology α] :
    TotallySeparatedSpace α :=
  ⟨fun _ _ b _ h =>
    ⟨{ b }ᶜ, { b }, isOpen_discrete _, isOpen_discrete _, h, rfl, (compl_union_self _).symm.subset,
      disjoint_compl_left⟩⟩

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