Theorem Order.IsPredLimit.lt_sub_natCast

Modification history

2024-12-06 17:36

Mathlib/Algebra/Order/SuccPred.lean

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

Added Order.IsPredLimit.lt_sub_natCast View on Github →