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.

source
@[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
source
theorem Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Ici a)
source
@[deprecated Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE (since := "2024-12-22")]
theorem Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Ici {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Ici a)

Alias of Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsGE.

source
theorem Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Iic a)
source
@[deprecated Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE (since := "2024-12-22")]
theorem Set.compl_section_ordSeparatingSet_mem_nhdsWithin_Iic {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhdsWithin a (Iic a)

Alias of Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhdsLE.

source
theorem Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhds {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhds a
source
@[deprecated Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhds (since := "2024-12-22")]
theorem Set.compl_section_ordSeparatingSet_mem_nhds {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {a : X} {s t : Set X} (hd : Disjoint s (closure t)) (ha : a ∈ s) :
(s.ordSeparatingSet t).ordConnectedSectionᶜ ∈ nhds a

Alias of Set.compl_ordConnectedSection_ordSeparatingSet_mem_nhds.

source
theorem Set.ordT5Nhd_mem_nhdsSet {X : Type u_1} [LinearOrder X] [TopologicalSpace X] [OrderTopology X] {s t : Set X} (hd : Disjoint s (closure t)) :
s.ordT5Nhd t ∈ nhdsSet s
source
@[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.

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