Theorem Order.not_isMax_pred

Modification history

2026-05-01 14:40

Mathlib/Order/SuccPred/Basic.lean

chore(Order/SuccPred/Basic): use `to_dual` more (#38653)

Deleted Order.not_isMax_pred View on Github →

2024-09-12 06:16

Mathlib/Order/SuccPred/Basic.lean

feat(Order/SuccPred/Limit): `IsSuccLimit` (#16499) …

Added Order.not_isMax_pred View on Github →