midpoint_zero_add — Mathlib

English

In a vector space V over R with invertible 2, the midpoint of 0 and x + y equals the midpoint of x and y for all x,y ∈ V.

Русский

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

LaTeX

$$$ \operatorname{midpoint} R 0 (x + y) = \operatorname{midpoint} R x y $$$

Lean4

theorem midpoint_zero_add (x y : V) : midpoint R 0 (x + y) = midpoint R x y :=
  (midpoint_eq_midpoint_iff_vsub_eq_vsub R).2 <| by simp

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