Theorems · Inductive type · order theory

ConditionallyCompleteLinearOrderBot

Type u_5 → Type u_5

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.

Defined in

Mathlib.Order.ConditionallyCompleteLattice.Defs

Cited by

84 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms