Mathlib v3 is deprecated. Go to Mathlib v4

Theorem order.lt_succ_bot_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.lt_succ_bot_iffView on Github →