lineMap_vsub_lineMap — Mathlib

English

The difference of two line maps equals the line map of the pairwise differences of endpoints: lineMap(p1,p2,c) − lineMap(p3,p4,c) = lineMap(p1 − p3, p2 − p4, c).

Русский

Разность двух линейных отображений по одним и тем же параметрам равна линейному отображению, построенному по попарным разницам концов: lineMap(p1,p2,c) − lineMap(p3,p4,c) = lineMap(p1 − p3, p2 − p4, c).

LaTeX

$$$ lineMap(p_1,p_2,c) -\\!_{v} lineMap(p_3,p_4,c) = lineMap(p_1 -\\!_{v} p_3, p_2 -\\!_{v} p_4, c) $$$

Lean4

theorem lineMap_vsub_lineMap (p₁ p₂ p₃ p₄ : P1) (c : k) :
    lineMap p₁ p₂ c -ᵥ lineMap p₃ p₄ c = lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄) c :=
  ((fst : P1 × P1 →ᵃ[k] P1) -ᵥ (snd : P1 × P1 →ᵃ[k] P1)).apply_lineMap (_, _) (_, _) c

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