Commit 2026-09-17 16:25 4db5fa78
View on Github →feat(Order/CompactlyGenerated/Basic): atoms are compact in a frame (#43402)
... and therefore an atomistic frame is compactly generated. This allows to synthesise IsCompactlyGenerated (Set α). Along the way we generalise a handful of results from CompleteLattice to SemilatticeSup.