Theorem sSup_ne_top

Modification history

2026-06-13 13:42

Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

feat(Order/ConditionallyCompleteLattice/Finset): `sSup s ≠ ⊤` in a `CompleteLinearOrder` for a finite set without `⊤` (#38356) …

Added sSup_ne_top View on Github →