Theorems · Definition · order theory

Set.ordConnectedComponent

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

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. Note that it is empty if and only if x ∉ s.

Defined in

Mathlib.Order.Interval.Set.OrdConnectedComponent

Cited by

23 results in Mathlib

Foundations

Depth 17 from the axioms · uses propext

Assumes

LinearOrder