Theorems · Definition · order theory

DedekindCut.factorEmbedding

{α : Type u_1} → {β : Type u_2} → [inst : CompleteLattice α] → [inst_1 : PartialOrder β] → β ↪o α → DedekindCut β ↪o α

Any order embedding β ↪o α into a complete lattice α factors through DedekindCut β. This map is defined so that factorEmbedding f A = sSup (f '' A.left). Although the construction factorEmbedding f A = sInf (f '' A.right) would also work, these do not in general give equal embeddings.

Defined in

Mathlib.Order.Completion

Cited by

3 results in Mathlib

Foundations

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

Assumes

CompleteLatticePartialOrder