Theorem WithBot.orderSucc_bot

Modification history

2026-05-01 14:40
Mathlib/Order/SuccPred/Basic.lean
chore(Order/SuccPred/Basic): use `to_dual` more (#38653)
Deleted WithBot.orderSucc_botView on Github →
2024-12-20 15:29
Mathlib/Order/SuccPred/Basic.lean
feat: the successor as a function `WithBot α → α` (#20055) …
Added WithBot.orderSucc_botView on Github →