midpoint_add_self — Mathlib

English

In a vector space V over R where 2 is invertible, for all x,y in V, 2 times the midpoint of x and y equals x + y.

Русский

Векторное пространство V над кольцом R с обратимым числом 2. Для любых x,y ∈ V выполняется 2 · midpoint(x,y) = x + y.

LaTeX

$$$ 2 \cdot \operatorname{midpoint} R x y = x + y $$$

Lean4

@[simp]
theorem midpoint_add_self (x y : V) : midpoint R x y + midpoint R x y = x + y :=
  calc
    midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x := by rw [midpoint_comm]
    _ = x + y := by rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]

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