Theorems · Definition · order theory

Set.ordSeparatingSet

{α : Type u_1} → [LinearOrder α] → Set α → Set α → Set α

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.

Defined in

Mathlib.Order.Interval.Set.OrdConnectedComponent

Cited by

8 results in Mathlib

Foundations

Depth 18 from the axioms · uses propext

Assumes

LinearOrder