vsub_lineMap — Mathlib

English

The difference between a point and a line map equals the line map of the differences.

Русский

Разность между точкой и отображением прямой равна отображению прямой через разности.

LaTeX

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

Lean4

theorem vsub_lineMap (p₁ p₂ p₃ : P₁) (c : k) : p₁ -ᵥ lineMap p₂ p₃ c = lineMap (p₁ -ᵥ p₂) (p₁ -ᵥ p₃) c :=
  (constVSub k p₁).apply_lineMap p₂ p₃ c

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