lift_snd_comp_fst_comp — Mathlib

English

For W,X,Y,Z and g: W → X, g': Y → Z, lift (snd_WY ≫ g') (fst_WY ≫ g) = (β_{W,Y}).hom ≫ (g' ⊗ g).

Русский

Для W,X,Y,Z и гомоморфизмов g: W→X, g': Y→Z: lift (snd_WY ≫ g') (fst_WY ≫ g) = (β_{W,Y}).hom ≫ (g' ⊗ g).

LaTeX

$$lift (snd W Y \;≫\; g') (fst W Y \;≫\; g) = (β_{W Y}).hom \;≫\; (g' \otimes g)$$

Lean4

@[simp, reassoc]
theorem lift_snd_comp_fst_comp {W X Y Z : C} (g : W ⟶ X) (g' : Y ⟶ Z) :
    lift (snd _ _ ≫ g') (fst _ _ ≫ g) = (β_ _ _).hom ≫ (g' ⊗ₘ g) := by cat_disch

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