comp_lift — Mathlib

English

For binary products, and morphisms f: V→W, g: W→X, h: W→Y, the composition f ≫ prod.lift g h equals prod.lift (f ≫ g) (f ≫ h).

Русский

Для двоичных произведений и морфизмов f: V→W, g: W→X, h: W→Y выполнено равенство: f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h).

LaTeX

$$$ f \\;\\;\\; prod.lift g h = prod.lift (f g) (f h) $$$

Lean4

@[reassoc, simp]
theorem comp_lift {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
    f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h) := by ext <;> simp

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