gradeMinOrder — Mathlib

English

If GradeMaxOrder 𝕆 α holds, then the dual order 𝕆ᵒᵈ αᵒᵈ carries a GradeMinOrder structure; conversely, GradeMinOrder on OrderDual induces GradeMaxOrder on the original.

Русский

Если существует GradeMaxOrder 𝕆 α, то у OrderDual 𝕆 αᵒᵈ есть GradeMinOrder; обратно GradeMinOrder на OrderDual порождает GradeMaxOrder на исходной структуре.

LaTeX

$$$[GradeMaxOrder 𝕆 α] \\Rightarrow [GradeMinOrder (OrderDual 𝕆) (OrderDual α)]$$$

Lean4

instance gradeMinOrder [GradeMaxOrder 𝕆 α] : GradeMinOrder 𝕆ᵒᵈ αᵒᵈ :=
  { OrderDual.gradeOrder with isMin_grade := fun _ => IsMax.grade (α := α) 𝕆 }

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