Commit 2026-01-23 14:21 599c3e6a

View on Github →

feat(Data/Nat/Lattice): ¬BddAbove s → sSup s = 0 (#33254)

Estimated changes

Modified Mathlib/Data/Int/ConditionallyCompleteOrder.lean

added theorem Int.csInf_eq_leastOfBdd

deleted theorem Int.csInf_eq_least_of_bdd

added theorem Int.csInf_of_not_bddBelow

deleted theorem Int.csInf_of_not_bdd_below

added theorem Int.csSup_eq_greatestOfBdd

deleted theorem Int.csSup_eq_greatest_of_bdd

added theorem Int.csSup_of_not_bddAbove

deleted theorem Int.csSup_of_not_bdd_above

Modified Mathlib/Data/Nat/Lattice.lean

added theorem Nat.sSup_of_not_bddAbove