Structures · Order

ConditionallyCompleteLinearOrder

A conditionally complete linear order is a linear order in which every nonempty subset which is bounded above has a supremum, and every nonempty subset which is bounded below has an infimum. Typical examples are real numbers or natural numbers. To differentiate the statements from the corresponding statements in (unconditional) complete linear orders, we prefix sInf and sSup by a c everywhere. The same statements should hold in both worlds, sometimes with additional assumptions of nonemptiness or boundedness.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Defs

Shape

One type argument · adds le_total, toDecidableLE, toDecidableEq, toDecidableLT, csSup_of_not_bddAbove, csInf_of_not_bddBelow, compare_eq_compareOfLessAndEq