Theorem Int.csInf_of_not_bddBelow

Modification history

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