midpoint_vsub_left — Mathlib

English

The v-subtraction from the left equals half of the left difference: p1 -ᵥ midpoint(R,p1,p2) = (1/2) • (p1 -ᵥ p2).

Русский

Из левой разности следует, что p1 -ᵥ середина(p1,p2) = (1/2) • (p1 -ᵥ p2).

LaTeX

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

Lean4

@[simp]
theorem midpoint_vsub_left (p₁ p₂ : P) : midpoint R p₁ p₂ -ᵥ p₁ = (⅟2 : R) • (p₂ -ᵥ p₁) :=
  lineMap_vsub_left _ _ _

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