ι_fromFreeYonedaCoproduct — Mathlib

English

For any m in M.Elements, the composition of the injection into the free Yoneda coproduct followed by the projection to M is exactly m.fromFreeYoneda.

Русский

Для любого m ∈ M.Elements композиция внедрения в свободный Coproduct Yoneda затем проекция на M равна m.fromFreeYoneda.

LaTeX

$$$M.\\iotaFreeYonedaCoproduct(m) \\; ;\\; M.fromFreeYonedaCoproduct = m.fromFreeYoneda$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_fromFreeYonedaCoproduct (m : M.Elements) :
    M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda := by apply Sigma.ι_desc

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