vsub_midpoint — Mathlib

English

Equality of midpoints is equivalent to equality of their pair of differences: midpoint(R,x,y)=midpoint(R,x',y') iff x -ᵥ x' = y' -ᵥ y.

Русский

Равенство середины двух пар эквивалентно равенству их векторных разностей: midpoint(R,x,y)=midpoint(R,x',y') ⇔ x -ᵥ x' = y' -ᵥ y.

LaTeX

$$$ \\operatorname{midpoint}(R,x,y) = \\operatorname{midpoint}(R,x',y') \\iff x -_{\\mathrm{v}} x' = y' -_{\\mathrm{v}} y $$$

Lean4

theorem vsub_midpoint (p₁ p₂ p : P) : p -ᵥ midpoint R p₁ p₂ = (⅟2 : R) • (p -ᵥ p₁) + (⅟2 : R) • (p -ᵥ p₂) := by
  rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    neg_vsub_eq_vsub_rev]

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