instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace

English

A prespectral T2 space is totally separated.

Русский

Пресspectral пространства типа T2 надлежит быть полностью раздельными.

LaTeX

$$$[\\mathrm{T2Space}(X)] \\land [\\mathrm{PrespectralSpace}(X)] \\Rightarrow \\mathrm{TotallySeparatedSpace}(X)$$$

Lean4

instance (priority := low) [T2Space X] [PrespectralSpace X] : TotallySeparatedSpace X :=
  totallySeparatedSpace_iff_exists_isClopen.mpr fun _ _ hxy ↦
    have ⟨U, ⟨hU₁, hU₂⟩, hxU, hyU⟩ := isTopologicalBasis.exists_subset_of_mem_open hxy isClosed_singleton.isOpen_compl
    ⟨U, ⟨hU₂.isClosed, hU₁⟩, hxU, fun h ↦ hyU h rfl⟩

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