comp_coprod — Mathlib

English

The first projection equals the coprod of the identity on M and the zero map: fst = id × 0.

Русский

Первая проекция равна копродукту тождественного отображения на M и нулевого отображения: fst = id × 0.

LaTeX

$$$ fst\\, R\\, M\\, M_2 = \\mathrm{coprod}\\,\\mathrm{id}_M\\, 0 $$$

Lean4

theorem comp_coprod (f : M₃ →ₗ[R] M₄) (g₁ : M →ₗ[R] M₃) (g₂ : M₂ →ₗ[R] M₃) :
    f.comp (g₁.coprod g₂) = (f.comp g₁).coprod (f.comp g₂) :=
  ext fun x => f.map_add (g₁ x.1) (g₂ x.2)

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