lift_fst_comp_snd_comp — Mathlib

English

For g: W → X and g': Y → Z, we have lift( fst ∘ g, snd ∘ g') = map g g'.

Русский

Пусть g: W → X и g': Y → Z. Тогда lift( fst ∘ g, snd ∘ g') = map g g'.

LaTeX

$$$prod.lift(prod.fst ∘ g, prod.snd ∘ g') = prod.map g g'$$$

Lean4

@[simp]
theorem lift_fst_comp_snd_comp {W X Y Z : C} [HasBinaryProduct W Y] [HasBinaryProduct X Z] (g : W ⟶ X) (g' : Y ⟶ Z) :
    prod.lift (prod.fst ≫ g) (prod.snd ≫ g') = prod.map g g' :=
  by
  rw [← prod.lift_map]
  simp
    -- We take the right-hand side here to be simp normal form, as this way composition lemmas for
    -- `f ≫ h` and `g ≫ k` can fire (e.g. `id_comp`), while `map_fst` and `map_snd` can still work just
    -- as well.

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