Commit 2026-06-13 13:42 bf69091c
View on Github →feat(Order/ConditionallyCompleteLattice/Finset): sSup s ≠ ⊤ in a CompleteLinearOrder for a finite set without ⊤ (#38356)
and more generally, sSup s ≠ a for a finite set s without a, when a ≠ ⊥.
Also adds the equivalent sInf/iSup/iInf lemmas.