Def Lattice.ofIsLUBofIsGLB

Modification history

2026-03-27 05:32
Mathlib/Order/Bounds/Basic.lean
feat: `SemilatticeSup.ofIsLUB`, `Lattice.ofIsLUBofIsGLB` (#37079)
Added Lattice.ofIsLUBofIsGLBView on Github →