right_vsub_midpoint — Mathlib

English

Symmetric right-variation equality: p2 -ᵥ midpoint(R,p1,p2) = (1/2) • (p2 -ᵥ p1).

Русский

Симметрично правая вариация: p2 -ᵥ середина(R,p1,p2) = (1/2) • (p2 -ᵥ p1).

LaTeX

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

Lean4

@[simp]
theorem right_vsub_midpoint (p₁ p₂ : P) : p₂ -ᵥ midpoint R p₁ p₂ = (⅟2 : R) • (p₂ -ᵥ p₁) := by
  rw [midpoint_comm, left_vsub_midpoint]

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