homMk'_comp — Mathlib

English

If f : S ⟶ T.obj Y, g : f.right ⟶ Y', g' : Y' ⟶ Y'', then

Русский

Если f : S ⟶ T.obj Y, g : f.right ⟶ Y', g' : Y' ⟶ Y'', то

LaTeX

$$$homMk'(f)\ (g \circ g') = homMk'(f)\ g \\ \circ\; homMk'\,(mk (f.hom \circ T.map g))\ g' \circ \mathrm{eqToHom}(\text{by simp})$$$

Lean4

theorem homMk'_comp (f : StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') :
    homMk' f (g ≫ g') = homMk' f g ≫ homMk' (mk (f.hom ≫ T.map g)) g' ≫ eqToHom (by simp) := by simp [eqToHom_right]

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