lineMap_vadd_lineMap — Mathlib

English

The sum of two line maps parameterized by the same c equals the line map of the sums: lineMap(v1,v2,c) + lineMap(p1,p2,c) = lineMap(v1+p1, v2+p2, c).

Русский

Сумма двух линейных отображений вдоль одной прямой равна линейному отображению от сумм начальных точек и концов: lineMap(v1,v2,c) + lineMap(p1,p2,c) = lineMap(v1+p1, v2+p2, c).

LaTeX

$$$ lineMap(v_1,v_2,c) +\\!_{v} lineMap(p_1,p_2,c) = lineMap(v_1 +\\!_{v} p_1, v_2 +\\!_{v} p_2, c) $$$

Lean4

theorem lineMap_vadd_lineMap (v₁ v₂ : V1) (p₁ p₂ : P1) (c : k) :
    lineMap v₁ v₂ c +ᵥ lineMap p₁ p₂ c = lineMap (v₁ +ᵥ p₁) (v₂ +ᵥ p₂) c :=
  ((fst : V1 × P1 →ᵃ[k] V1) +ᵥ (snd : V1 × P1 →ᵃ[k] P1)).apply_lineMap (v₁, p₁) (v₂, p₂) c

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