English
WithBot α carries a SuccOrder structure, defined by: ⊥ maps to ⊥, and each ↑a maps to succ a; and related relations transfer accordingly.
Русский
WithBot α имеет структуру SuccOrder, задаваемую: ⊥ → ⊥, ↑a → succ(a) и сопутствующие связи переносятся.
LaTeX
$$$$ \text{SuccOrder}(WithBot(\\alpha)) \\text{ defined by } \\operatorname{succ}(\\bot) = \\bot, \\operatorname{succ}(\\iota(a)) = \\iota(\\operatorname{succ}(a)). $$$$
Lean4
instance : SuccOrder (WithBot α)
where
succ
a :=
match a with
| ⊥ => some ⊥
| Option.some a => some (succ a)
le_succ
a :=
match a with
| ⊥ => bot_le
| Option.some a => coe_le_coe.2 (le_succ a)
max_of_succ_le {a}
ha := by
cases a
· exact ((bot_lt_coe (⊥ : α)).not_ge ha).elim
· exact (max_of_succ_le <| coe_le_coe.1 ha).withBot
succ_le_of_lt {a b}
h := by
cases b
· exact (not_lt_bot h).elim
cases a
· exact coe_le_coe.2 bot_le
· exact coe_le_coe.2 (succ_le_of_lt <| coe_lt_coe.1 h)
