Documentation

Mathlib.Topology.Order.T5

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]

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

Equations
  • =
@[instance 100]
Equations
  • =