English
There is a PredOrder structure on the dual order αᵒᵈ induced from a SuccOrder structure on α, defined by pred = toDual ∘ SuccOrder.succ ∘ ofDual.
Русский
На двойственном порядке αᵒᵈ задаётся структура PredOrder, полученная из SuccOrder α, предикат pred определяется как toDual ∘ SuccOrder.succ ∘ ofDual.
LaTeX
$$$\\text{PredOrder}(\\alpha^{\\mathrm{op}}) \\text{ создан из } \\text{SuccOrder}(\\alpha) \\text{ через } \\text{pred} = \\mathrm{toDual} \\circ \\mathrm{SuccOrder.succ} \\circ \\mathrm{ofDual}.$$$
Lean4
instance [Preorder α] [SuccOrder α] : PredOrder αᵒᵈ
where
pred := toDual ∘ SuccOrder.succ ∘ ofDual
pred_le := by simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual, SuccOrder.le_succ, implies_true]
min_of_le_pred h := by apply SuccOrder.max_of_succ_le h
le_pred_of_lt := by intro a b h; exact SuccOrder.succ_le_of_lt h
