Theorem iSup_ne_of_notMem

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 iSup_ne_of_notMem View on Github →