Commit 2026-09-08 06:43 e861750b
View on Github →feat(Order): characterise compact elements in atomistic lattices (#43530)
... as those elements that are the suprema of finitely many atoms.
Also make the type variable correctly implicit in most lemmas and move declarations out of the CompleteLattice namespace.