midpoint_vsub_midpoint_same_right

English

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

Русский

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

LaTeX

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

Lean4

theorem midpoint_vsub_midpoint_same_right (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, add_zero]

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