Linear order is a completely normal Hausdorff topological space #
In this file we prove that a linear order with order topology is a completely normal Hausdorff topological space.
@[simp]
theorem
Set.ordConnectedComponent_mem_nhds
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{s : Set X}
:
theorem
Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Ici
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{s : Set X}
{t : Set X}
(hd : Disjoint s (closure t))
(ha : a ∈ s)
:
(Set.ordConnectedSection (Set.ordSeparatingSet s t))ᶜ ∈ nhdsWithin a (Set.Ici a)
theorem
Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Iic
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{s : Set X}
{t : Set X}
(hd : Disjoint s (closure t))
(ha : a ∈ s)
:
(Set.ordConnectedSection (Set.ordSeparatingSet s t))ᶜ ∈ nhdsWithin a (Set.Iic a)
theorem
Set.compl_section_ordSeparatingSet_mem_nhds
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{a : X}
{s : Set X}
{t : Set X}
(hd : Disjoint s (closure t))
(ha : a ∈ s)
:
(Set.ordConnectedSection (Set.ordSeparatingSet s t))ᶜ ∈ nhds a
theorem
Set.ordT5Nhd_mem_nhdsSet
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
{s : Set X}
{t : Set X}
(hd : Disjoint s (closure t))
:
Set.ordT5Nhd s t ∈ nhdsSet s
instance
OrderTopology.t5Space
{X : Type u_1}
[LinearOrder X]
[TopologicalSpace X]
[OrderTopology X]
:
T5Space X
A linear order with order topology is a completely normal Hausdorff topological space.