lineMap_vsub — Mathlib

English

Subtracting a fixed point from the line mapping corresponds to shifting both endpoints.

Русский

Вычитание фиксированной точки из отображения линии соответствует сдвигу обоих концов.

LaTeX

$$p1 -ᵥ lineMap p2 p3 c = lineMap (p1 -ᵥ p2) (p1 -ᵥ p3) c$$

Lean4

theorem lineMap_vsub (p₁ p₂ p₃ : P₁) (c : k) : lineMap p₁ p₂ c -ᵥ p₃ = lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₃) c :=
  (vaddConst k p₃).symm.apply_lineMap p₁ p₂ c

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