Structures · Order

ConditionallyCompleteLattice

A conditionally complete lattice is a lattice 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 lattices, 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 isLUB_csSup, isGLB_csInf