Theorems · Definition · order theory

DedekindCut.principalIso

{α : Type u_1} → [inst : CompleteLattice α] → α ≃o DedekindCut α

DedekindCut.principal as an OrderIso. This provides the second half of the fundamental theorem of concept lattices: every complete lattice is isomorphic to a concept lattice (its own Dedekind completion). See Concept.instCompleteLattice for the first half.

Defined in

Mathlib.Order.Completion

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CompleteLattice