Commit 2024-12-11 14:33 2c66a575

View on Github →

feat(Order/SuccPred/Limit): extra lemmas (#19801) These are trivial variations on already proven results.

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredLimit.le_iff_forall_le

added theorem Order.IsPredLimit.lt_iff_exists_lt

added theorem Order.IsPredLimit.pred_le_iff

added theorem Order.IsPredPrelimit.pred_le_iff

added theorem Order.IsSuccLimit.le_iff_forall_le

added theorem Order.IsSuccLimit.le_succ_iff

added theorem Order.IsSuccLimit.lt_iff_exists_lt

added theorem Order.IsSuccPrelimit.le_succ_iff