lineMap_vadd — Mathlib

English

When translating along a line, adding a point p before or after the line map shifts consistently.

Русский

При переносе вдоль прямой, добавление точки p до или после отображения линии сохраняет согласованность.

LaTeX

$$lineMap v v' c +ᵥ p = lineMap (v +ᵥ p) (v' +ᵥ p) c$$

Lean4

theorem lineMap_vadd (v v' : V₁) (p : P₁) (c : k) : lineMap v v' c +ᵥ p = lineMap (v +ᵥ p) (v' +ᵥ p) c :=
  (vaddConst k p).apply_lineMap v v' c

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