midpoint_vadd_midpoint — Mathlib

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 _ _ _ _ _

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