Theorems · Inductive type · order theory

ConditionallyCompleteLattice

Type u_5 → Type u_5

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

Cited by

364 results in Mathlib

Foundations

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