Commit 2024-12-06 17:36 75b9e913

View on Github →

feat(Algebra/Order/SuccPred): IsSuccLimit theorems for SuccAddOrder (#19060)

Estimated changes

Modified Mathlib/Algebra/Order/SuccPred.lean

added theorem Order.IsPredLimit.lt_sub_natCast

added theorem Order.IsPredLimit.lt_sub_one

added theorem Order.IsPredPrelimit.lt_sub_natCast

added theorem Order.IsPredPrelimit.lt_sub_one

added theorem Order.IsSuccLimit.add_natCast_lt

added theorem Order.IsSuccLimit.add_one_lt

added theorem Order.IsSuccPrelimit.add_natCast_lt

added theorem Order.IsSuccPrelimit.add_one_lt

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.lt_top