coe_weight_mk — Mathlib

English

For any χ and h, the weight χ is embedded in a Weight object with corresponding function χ, i.e., coe (⟨χ,h⟩) is χ.

Русский

Для любого χ и h, вес χ отображается в объект Weight с соответствующей функцией χ; коэрц (⟨χ, h⟩) равен χ.

LaTeX

$$$ (\\mathrm{Weight}\\;R\\;L\\;M) \\ni (χ,h) \\mapsto χ $$$

Lean4

@[simp]
theorem coe_weight_mk (χ : L → R) (h) : (↑(⟨χ, h⟩ : Weight R L M) : L → R) = χ :=
  rfl

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