Theorem Int.csSup_of_not_bddAbove

Modification history

2026-01-23 14:21
Mathlib/Data/Int/ConditionallyCompleteOrder.lean
feat(Data/Nat/Lattice): `¬BddAbove s → sSup s = 0` (#33254)
Added Int.csSup_of_not_bddAboveView on Github →