fromFreeYonedaCoproduct_app_mk — Mathlib

English

For m in M.Elements, the equation M.fromFreeYonedaCoproduct.app m.fst on the coproduct's canonical element equals m.snd, i.e., the canonical component recovers the original data.

Русский

Для m ∈ M.Elements уравнение M.fromFreeYonedaCoproduct.app m.fst на каноническом элементе копродукта равно m.snd, то есть канонический компонент восстанавливает исходные данные.

LaTeX

$$$M.fromFreeYonedaCoproduct.app m.fst (\\text{canonical}) = m.snd$$$

Lean4

@[simp]
theorem fromFreeYonedaCoproduct_app_mk (m : M.Elements) :
    M.fromFreeYonedaCoproduct.app _ (M.freeYonedaCoproductMk m) = m.2 :=
  by
  dsimp [freeYonedaCoproductMk]
  erw [M.ι_fromFreeYonedaCoproduct_apply m]
  rw [m.fromFreeYoneda_app_apply]

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