Commit 2024-09-23 19:41 c1332699

View on Github →

feat(Order/SuccPred/Limit): IsSuccPrelimit.le_iff_forall_le (#17026)

Estimated changes

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsPredPrelimit.le_iff_forall_le

added theorem Order.IsPredPrelimit.lt_iff_exists_lt

added theorem Order.IsSuccPrelimit.le_iff_forall_le

added theorem Order.IsSuccPrelimit.lt_iff_exists_lt