Theorem Order.IsPredLimit.pred_le_iff

Modification history

2025-12-26 22:32
Mathlib/Order/SuccPred/Limit.lean
chore: use `to_dual` on `IsSuccPrelimit` / `IsSuccLimit` (#33151)
Deleted Order.IsPredLimit.pred_le_iffView on Github →
2024-12-11 14:33
Mathlib/Order/SuccPred/Limit.lean
feat(Order/SuccPred/Limit): extra lemmas (#19801) …
Added Order.IsPredLimit.pred_le_iffView on Github →