Theorem Int.csSup_eq_greatestOfBdd

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_eq_greatestOfBddView on Github →