Theorem Order.IsPredPrelimit.lt_sub_one

Modification history

2024-12-06 17:36

Mathlib/Algebra/Order/SuccPred.lean

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

Added Order.IsPredPrelimit.lt_sub_one View on Github →