hom_comp_ι — Mathlib

English

For multifork homomorphisms f: K1 → K2, we have f.hom ≫ K2.ι j = K1.ι j for every index j in J.L.

Русский

Для гомоморфизмов между мульфорами: f.hom ≫ K2.ι j = K1.ι j для каждого j из J.L.

LaTeX

$$$\forall {K_1 K_2 : Multifork I} \; (f : K_1 ⟶ K_2) \; (j : J.L),\; f.hom ≫ K_2.\mathrm{ι} j = K_1.\mathrm{ι} j$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_comp_ι (K₁ K₂ : Multifork I) (f : K₁ ⟶ K₂) (j : J.L) : f.hom ≫ K₂.ι j = K₁.ι j :=
  f.w _

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