Commit 2026-03-27 05:32 abdd9d64

View on Github →

feat: SemilatticeSup.ofIsLUB, Lattice.ofIsLUBofIsGLB (#37079)

Estimated changes

Modified Mathlib/Order/Bounds/Basic.lean

added def Lattice.ofIsLUBofIsGLB

added def SemilatticeSup.ofIsLUB

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

deleted def conditionallyCompleteLatticeOfLatticeOfsInf

deleted def conditionallyCompleteLatticeOfsInf