Theorem Int.csInf_eq_leastOfBdd

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