comp_fst_add_comp_snd — Mathlib

English

The linear combination of the compositions with fst and snd equals the coprod: f1.comp fst + f2.comp snd = f1.coprod f2.

Русский

Линейная комбинация композиций с fst и snd равна coprod: f1.comp fst + f2.comp snd = f1.coprod f2.

LaTeX

$$$$ f_1.comp(\text{fst}) + f_2.comp(\text{snd}) = f_1.coprod f_2 $$$$

Lean4

theorem comp_fst_add_comp_snd (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M) :
    f₁.comp (.fst _ _ _) + f₂.comp (.snd _ _ _) = f₁.coprod f₂ :=
  rfl

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