midpoint_vsub_right — Mathlib

English

The right v-subtraction gives the same half-difference symmetry: p2 -ᵥ midpoint(R,p1,p2) = (1/2) • (p2 -ᵥ p1).

Русский

Правая v-sub выражает ту же симметрию: 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 midpoint_vsub_right (p₁ p₂ : P) : midpoint R p₁ p₂ -ᵥ p₂ = (⅟2 : R) • (p₁ -ᵥ p₂) := by
  rw [midpoint_comm, midpoint_vsub_left]

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