Theorem Order.IsSuccPrelimit.add_one_lt

Modification history

2024-12-06 17:36

Mathlib/Algebra/Order/SuccPred.lean

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

Added Order.IsSuccPrelimit.add_one_lt View on Github →