Order connected components of a set #
In this file we define Set.ordConnectedComponent s x
to be the set of y
such that
Set.uIcc x y ⊆ s⊆ s
and prove some basic facts about this definition. At the moment of writing,
this construction is used only to prove that any linear order with order topology is a T₅ space,
so we only add API needed for this lemma.
Order-connected component of a point x
in a set s
. It is defined as the set of y
such that
Set.uIcc x y ⊆ s⊆ s
. Note that it is empty if and only if x ∉ s∉ s
.
Equations
- Set.ordConnectedComponent s x = { y | Set.uIcc x y ⊆ s }
Equations
- One or more equations did not get rendered due to their size.
Projection from s : Set α
to α
sending each order connected component of s
to a single
point of this component.
Equations
- Set.ordConnectedProj s x = Set.Nonempty.some (_ : Set.Nonempty (Set.ordConnectedComponent s ↑x))
A set that intersects each order connected component of a set by a single point. Defined as the
range of Set.ordConnectedProj s
.
Equations
Given two sets s t : Set α
, the set Set.orderSeparatingSet s t
is the set of points that
belong both to some Set.ordConnectedComponent tᶜ x
, x ∈ s∈ s
, and to some
Set.ordConnectedComponent sᶜ x
, x ∈ t∈ t
. In the case of two disjoint closed sets, this is the
union of all open intervals $(a, b)$ such that their endpoints belong to different sets.
Equations
- Set.ordSeparatingSet s t = (Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (tᶜ) x) ∩ Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (sᶜ) x
An auxiliary neighborhood that will be used in the proof of OrderTopology.t5Space
.
Equations
- Set.ordT5Nhd s t = Set.unionᵢ fun x => Set.unionᵢ fun h => Set.ordConnectedComponent (tᶜ ∩ Set.ordConnectedSection (Set.ordSeparatingSet s t)ᶜ) x