English
For x, y ∈ s, ordConnectedProj s x = ordConnectedProj s y iff the order interval between x and y is contained in s.
Русский
Для x, y ∈ s, ordConnectedProj s x = ordConnectedProj s y тогда и только тогда, когда порядоковый интервал между x и y содержится в s.
LaTeX
$$$\operatorname{ordConnectedProj}(s, x) = \operatorname{ordConnectedProj}(s, y) \iff [[(x : \alpha), y]] \subseteq s$$$
Lean4
/-- 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`, and to some
`Set.ordConnectedComponent sᶜ x`, `x ∈ 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. -/
def ordSeparatingSet (s t : Set α) : Set α :=
(⋃ x ∈ s, ordConnectedComponent tᶜ x) ∩ ⋃ x ∈ t, ordConnectedComponent sᶜ x
