English
Translating both endpoints by vectors v and v' commutes with taking the midpoint.
Русский
Сдвиг обеих точек на векторы v и v' сохраняет середину: середина между переносами равна переносам середины.
LaTeX
$$$ \\operatorname{midpoint}(R, v, v') +_{\\mathrm{v}} \\operatorname{midpoint}(R, p, p') = \\operatorname{midpoint}(R, v+_{\\mathrm{v}} p,\\; v'+_{\\mathrm{v}} p') $$$
Lean4
theorem midpoint_vadd_midpoint (v v' : V) (p p' : P) :
midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p') :=
lineMap_vadd_lineMap _ _ _ _ _