Structures · Order

Set.OrdConnected

We say that a set s : Set α is OrdConnected if for all x y ∈ s it includes the interval [[x, y]]. If α is a DenselyOrdered ConditionallyCompleteLinearOrder with the OrderTopology, then this condition is equivalent to IsPreconnected s. If α is a linearly ordered field, then this condition is also equivalent to Convex α s.

Defined in

Mathlib.Order.Interval.Set.Defs

Shape

One type argument · adds out'