midpoint_eq_smul_add — Mathlib

English

In a vector space V over R with 2 invertible, the midpoint of x and y equals one half of (x + y).

Русский

Векторное пространство V над R, где 2 обратимо. Середина между x и y равна половине суммы x + y.

LaTeX

$$$ \operatorname{midpoint} R x y = \left( \tfrac{1}{2} : R \right) \cdot (x + y) $$$

Lean4

theorem midpoint_eq_smul_add (x y : V) : midpoint R x y = (⅟2 : R) • (x + y) := by
  rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ← two_smul R, smul_smul,
    mul_invOf_self, one_smul, add_sub_cancel_left]

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