grade_ofDual — Mathlib

English

There is a dual version of grade: grade 𝕆 (ofDual a) = ofDual( grade 𝕆ᵒᵈ a ).

Русский

Существует двойственная версия градации: grade 𝕆 (ofDual a) = ofDual( grade 𝕆ᵒᵈ a ).

LaTeX

$$$\\\\operatorname{grade}_{\\\\mathcal{O}}(\\\\mathrm{ofDual}(a)) = \\\\mathrm{ofDual}(\\\\operatorname{grade}_{\\\\mathcal{O}^\\\\mathrm{op}}(a))$$$

Lean4

@[simp]
theorem grade_ofDual [GradeOrder 𝕆 α] (a : αᵒᵈ) : grade 𝕆 (ofDual a) = ofDual (grade 𝕆ᵒᵈ a) :=
  rfl

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