grade_coe — Mathlib

English

For a flag a in α, the grade of its image matches the grade of the flag element itself.

Русский

Для элемента флага a ∈ α значение градации в α совпадает с градацией самого элемента флага.

LaTeX

$$$ \\operatorname{grade}(\\mathcal{O}, a:\\alpha) = \\operatorname{grade}(\\mathcal{O}, a). $$$

Lean4

@[simp, norm_cast]
theorem grade_coe [GradeOrder 𝕆 α] (a : s) : grade 𝕆 (a : α) = grade 𝕆 a :=
  rfl

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