right_sub_midpoint — Mathlib

English

Right-substitution identity for vectors and midpoint: v2 - midpoint(R,v1,v2) = (1/2) • (v2 - v1).

Русский

Правый вычет: v2 - середина(R,v1,v2) = (1/2) • (v2 - v1).

LaTeX

$$$ v_2 -_{\\mathrm{v}} \\operatorname{midpoint}(R,v_1,v_2) = \\left(\\tfrac{1}{2}\\right) \\cdot (v_2 -_{\\mathrm{v}} v_1) $$$

Lean4

@[simp]
theorem right_sub_midpoint (v₁ v₂ : V) : v₂ - midpoint R v₁ v₂ = (⅟2 : R) • (v₂ - v₁) :=
  right_vsub_midpoint v₁ v₂

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