grade_toDual — Mathlib

English

There is compatibility between grading and dualing: grade on the dual is the dual of grade on the original:

Русский

Существуют совместимости между градацией и двойственностью: градация на двойственном порядке равна двойственности градации на исходном порядке.

LaTeX

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

Lean4

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

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