English
WithTop α is equipped with a PredOrder structure extending that of α, with pred(⊤) = ⊤ and pred(↑a) = ↑(pred(a)); the remaining axioms adapt accordingly.
Русский
Для WithTop α определяется PredOrder, который расширяет PredOrder α, задавая pred(⊤)=⊤ и pred(↑a)=↑(pred(a)); остальные аксиомы применяются аналогично.
LaTeX
$$$$ \text{PredOrder}(WithTop(\\alpha)) \\text{ with } \\operatorname{pred}(\\top) = \\top, \\operatorname{pred}(\\iota(a)) = \\iota(\\operatorname{pred}(a)). $$$$
Lean4
instance : PredOrder (WithTop α)
where
pred
a :=
match a with
| ⊤ => some ⊤
| Option.some a => some (pred a)
pred_le
a :=
match a with
| ⊤ => le_top
| Option.some a => coe_le_coe.2 (pred_le a)
min_of_le_pred {a}
ha := by
cases a
· exact ((coe_lt_top (⊤ : α)).not_ge ha).elim
· exact (min_of_le_pred <| coe_le_coe.1 ha).withTop
le_pred_of_lt {a b}
h := by
cases a
· exact (le_top.not_gt h).elim
cases b
· exact coe_le_coe.2 le_top
exact coe_le_coe.2 (le_pred_of_lt <| coe_lt_coe.1 h)
