instTotallySeparatedSpaceOfDiscreteTopology

English

If X is discrete, then OnePoint X is totally separated.

Русский

Если X дискретно, то OnePoint X абсолютно разобщимо.

LaTeX

$$$\\text{TotallySeparatedSpace}(\\mathrm{OnePoint}(X))$ when X is discrete.$$

Lean4

instance (X : Type*) [TopologicalSpace X] [DiscreteTopology X] : TotallySeparatedSpace (OnePoint X) where
  isTotallySeparated_univ x _ y _
    hxy := by
    cases x with
    |
      infty =>
      refine
        ⟨{ y }ᶜ, { y }, isOpen_compl_singleton, ?_, hxy, rfl, (compl_union_self _).symm.subset, disjoint_compl_left⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, hxy]
    | coe
      val =>
      refine ⟨{some val}, {some val}ᶜ, ?_, isOpen_compl_singleton, rfl, hxy.symm, by simp, disjoint_compl_right⟩
      rw [OnePoint.isOpen_iff_of_notMem]
      exacts [isOpen_discrete _, (Option.some_ne_none val).symm]

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