comp_coprod — Mathlib

English

Composition distributes over coprod: f ∘ (g1 coprod g2) = (f ∘ g1) coprod (f ∘ g2).

Русский

Композиция распределяет Coprod: f ∘ (g1 coprod g2) = (f ∘ g1) coprod (f ∘ g2).

LaTeX

$$$$ f.comp(\,g_1.coprod g_2\,) = (f.comp g_1).coprod (f.comp g_2) $$$$

Lean4

theorem comp_coprod (f : M →L[R] N) (g₁ : M₁ →L[R] M) (g₂ : M₂ →L[R] M) :
    f.comp (g₁.coprod g₂) = (f.comp g₁).coprod (f.comp g₂) :=
  coe_injective <| LinearMap.comp_coprod ..

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