instSuccOrderOrderDualOfPredOrder

English

The dual construction induces the PredOrder structure with the corresponding lemmas for pred-related properties via the dualization of succ-order.

Русский

Двойственная конструкция порождает PredOrder со свойствами pred, вытекающими из дуализации порядка-следующего.

LaTeX

$$$\\text{PredOrder}(\\alpha^{\\mathrm{op}}) \\text{ via dualization of } \\text{SuccOrder}(\\alpha).$$$

Lean4

instance [Preorder α] [PredOrder α] : SuccOrder αᵒᵈ
    where
  succ := toDual ∘ PredOrder.pred ∘ ofDual
  le_succ := by simp only [comp, OrderDual.forall, ofDual_toDual, toDual_le_toDual, PredOrder.pred_le, implies_true]
  max_of_succ_le h := by apply PredOrder.min_of_le_pred h
  succ_le_of_lt := by intro a b h; exact PredOrder.le_pred_of_lt h

Похожие утверждения