left_vsub_midpoint — Mathlib

English

Translating the left-hand point by the midpoint yields a half-difference: p1 -ᵥ midpoint(R,p1,p2) = (1/2) • (p1 -ᵥ p2).

Русский

Сдвиг левой точки на середину приводит к половине разности: p1 -ᵥ середина(R,p1,p2) = (1/2) • (p1 -ᵥ p2).

LaTeX

$$$ p_1 -_{\\mathrm{v}} \\operatorname{midpoint}(R,p_1,p_2) = \\left(\\tfrac{1}{2}\\right) \\cdot (p_1 -_{\\mathrm{v}} p_2) $$$

Lean4

@[simp]
theorem left_vsub_midpoint (p₁ p₂ : P) : p₁ -ᵥ midpoint R p₁ p₂ = (⅟2 : R) • (p₁ -ᵥ p₂) :=
  left_vsub_lineMap _ _ _

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