instGradeBoundedOrderOrderDual — Mathlib

English

If α is a GradeBoundedOrder, then the dual structure on OrderDual 𝕆 and OrderDual α also forms a GradeBoundedOrder.

Русский

Если α —GradeBoundedOrder, то дуальная структура OrderDual 𝕆 на OrderDual α образует также GradeBoundedOrder.

LaTeX

$$$[GradeBoundedOrder 𝕆 α] \\Rightarrow [GradeBoundedOrder (OrderDual 𝕆) (OrderDual α)]$$$

Lean4

instance [GradeBoundedOrder 𝕆 α] : GradeBoundedOrder 𝕆ᵒᵈ αᵒᵈ :=
  { OrderDual.gradeMinOrder, OrderDual.gradeMaxOrder with }

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