Theorem Order.IsPredLimit.lt_top

Modification history

2025-12-26 22:32
Mathlib/Order/SuccPred/Limit.lean
chore: use `to_dual` on `IsSuccPrelimit` / `IsSuccLimit` (#33151)
Deleted Order.IsPredLimit.lt_topView on Github →
2024-12-06 17:36
Mathlib/Order/SuccPred/Limit.lean
feat(Algebra/Order/SuccPred): `IsSuccLimit` theorems for `SuccAddOrder` (#19060)
Added Order.IsPredLimit.lt_topView on Github →