Def PredOrder.ofLePredIff

Modification history

2026-03-21 08:07

Mathlib/Order/SuccPred/Basic.lean

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

Deleted PredOrder.ofLePredIff View on Github →

2023-01-01 19:51

Mathlib/Order/SuccPred/Basic.lean

feat: port Order.SuccPred.Basic (#1233) …

Added PredOrder.ofLePredIff View on Github →