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} : s.ordConnectedComponent a ∈ nhds a ↔ s ∈ nhds a

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) : (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 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) : (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 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) : (s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ 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)) : s.ordT5Nhd t ∈ nhdsSet s

@[instance 100]

instance OrderTopology.completelyNormalSpace {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] : CompletelyNormalSpace X

A linear order with order topology is a completely normal Hausdorff topological space.

Equations

• ⋯ = ⋯

@[instance 100]

instance OrderTopology.t5Space {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] : T5Space X

Equations

• ⋯ = ⋯