comp_inl_add_comp_inr — Mathlib

English

For L: M1×M2 →L[R] M3 and v: M1×M2, L.comp(inl) v1 + L.comp(inr) v2 equals L v.

Русский

Для линейного отображения L: M1×M2 → M3 и вектора v, имеем L∘inl(v1) + L∘inr(v2) = L(v).

LaTeX

$$$L.comp(\text{inl } R M_1 M_2)\, v.1 + L.comp(\text{inr } R M_1 M_2)\, v.2 = L\, v$$$

Lean4

theorem comp_inl_add_comp_inr (L : M₁ × M₂ →L[R] M₃) (v : M₁ × M₂) :
    L.comp (.inl R M₁ M₂) v.1 + L.comp (.inr R M₁ M₂) v.2 = L v := by simp [← map_add]

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