Commit 2026-02-10 16:30 e0c01c23

View on Github →

feat(Order/CompleteLattice/Defs): to_dual for CompleteSemilattices (#33765) This PR uses to_dual for CompleteSemilatticeSup and CompleteSemilatticeInf. These will need to be refactored/deprecated in the future, but I think it makes sense to make the code smaller (using to_dual) before such a refactor.

Estimated changes

deleted theorem iInf_le_iff
deleted theorem isGLB_iff_sInf_eq
deleted theorem isGLB_sInf
deleted theorem le_sInf
deleted theorem le_sInf_iff
deleted theorem ofDual_iInf
deleted theorem ofDual_sInf
deleted theorem sInf_le
deleted theorem sInf_le_iff
deleted theorem sInf_le_of_le
deleted theorem sInf_le_sInf
deleted theorem toDual_iInf
deleted theorem toDual_sInf