Linear order is a completely normal Hausdorff topological space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that a linear order with order topology is a completely normal Hausdorff topological space.
@[simp]
theorem
set.ord_connected_component_mem_nhds
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X]
{a : X}
{s : set X} :
theorem
set.compl_section_ord_separating_set_mem_nhds_within_Ici
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X]
{a : X}
{s t : set X}
(hd : disjoint s (closure t))
(ha : a ∈ s) :
(s.ord_separating_set t).ord_connected_sectionᶜ ∈ nhds_within a (set.Ici a)
theorem
set.compl_section_ord_separating_set_mem_nhds_within_Iic
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X]
{a : X}
{s t : set X}
(hd : disjoint s (closure t))
(ha : a ∈ s) :
(s.ord_separating_set t).ord_connected_sectionᶜ ∈ nhds_within a (set.Iic a)
theorem
set.compl_section_ord_separating_set_mem_nhds
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X]
{a : X}
{s t : set X}
(hd : disjoint s (closure t))
(ha : a ∈ s) :
theorem
set.ord_t5_nhd_mem_nhds_set
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X]
{s t : set X}
(hd : disjoint s (closure t)) :
s.ord_t5_nhd t ∈ nhds_set s
@[protected, instance]
def
order_topology.t5_space
{X : Type u_1}
[linear_order X]
[topological_space X]
[order_topology X] :
t5_space X
A linear order with order topology is a completely normal Hausdorff topological space.