Theorems · Inductive type · order theory

Set.OrdConnected

{α : Type u_1} → [Preorder α] → Set α → Prop

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

Cited by

161 results in Mathlib

Foundations

Depth 1 from the axioms, rests on 3 definitions · uses no axioms

Assumes

Preorder