Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order.pred_top_le_iff

Modification history

2022-07-31 20:14
src/order/succ_pred/basic.lean
feat(order/succ_pred/basic): `a ≤ succ ⊥ ↔ a = ⊥ ∨ a = succ ⊥` and related (#15567) …
Added order.pred_top_le_iffView on Github →