gradeMaxOrder — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

instance gradeMaxOrder [GradeMinOrder 𝕆 α] : GradeMaxOrder 𝕆ᵒᵈ αᵒᵈ :=
  { OrderDual.gradeOrder with isMax_grade := fun _ => IsMin.grade (α := α) 𝕆 }

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