Structures · Order

ConditionallyCompleteLinearOrderBot

A conditionally complete linear order with Bot is a linear order with least element, in which every nonempty subset which is bounded above has a supremum, and every nonempty subset (necessarily bounded below) has an infimum. A typical example is the 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.