midpoint_vsub_midpoint_same_left — Mathlib

English

For p1,p2,p3 in an affine space, the v-difference between midpoints with base p1 equals half of p2 − p3.

Русский

Для точек p1,p2,p3 в аффинном пространстве разность по вектору между серединами с опорой p1 равна половине разности p2 − p3.

LaTeX

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

Lean4

theorem midpoint_vsub_midpoint_same_left (p₁ p₂ p₃ : P) :
    midpoint R p₁ p₂ -ᵥ midpoint R p₁ p₃ = (⅟2 : R) • (p₂ -ᵥ p₃) := by
  rw [midpoint_vsub_midpoint, vsub_self, midpoint_eq_smul_add, zero_add]

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