English
A formula expressing the vector subtraction from a point to the midpoint in terms of p -ᵥ p1 and p -ᵥ p2.
Русский
Формула выражает векторную вычитание точки из середины через p -ᵥ p1 и p -ᵥ p2.
LaTeX
$$$ p -_{\\mathrm{v}} \\operatorname{midpoint}(R,p_1,p_2) = \\left(\\tfrac{1}{2}\\right) \\cdot (p -_{\\mathrm{v}} p_1) + \\left(\\tfrac{1}{2}\\right) \\cdot (p -_{\\mathrm{v}} p_2) $$$
Lean4
theorem midpoint_vsub (p₁ p₂ p : P) : midpoint R p₁ p₂ -ᵥ p = (⅟2 : R) • (p₁ -ᵥ p) + (⅟2 : R) • (p₂ -ᵥ p) := by
rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg, neg_vsub_eq_vsub_rev, add_assoc,
invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc, midpoint_comm, midpoint, lineMap_apply]
