midpoint_vsub_midpoint — Mathlib

English

Difference of midpoints equals the midpoint of the corresponding endpoint differences in the torsor.

Русский

Разность середины между p1 и p2 и середины между p3 и p4 равна середине разностей соответствующих пар точек в т最後орском пространстве.

LaTeX

$$$ \\operatorname{midpoint}(R,p_1,p_2) -_{\\mathrm{v}} \\operatorname{midpoint}(R,p_3,p_4) = \\operatorname{midpoint}(R, (p_1-_{\\mathrm{v}} p_3), (p_2-_{\\mathrm{v}} p_4)) $$$

Lean4

theorem midpoint_vsub_midpoint (p₁ p₂ p₃ p₄ : P) :
    midpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄) :=
  lineMap_vsub_lineMap _ _ _ _ _

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