right_vsub_lineMap — Mathlib

English

For p0, p1 in P1 and c in k, the vector from lineMap(p0, p1, c) to p1 equals (1 − c) times the vector from p0 to p1: p1 − lineMap(p0,p1,c) = (1 − c) · (p1 − p0).

Русский

Из p1 вычитаем lineMap(p0,p1,c): p1 − lineMap(p0,p1,c) = (1 − c) · (p1 − p0).

LaTeX

$$$ p_1 -\\!_{v} lineMap(p_0,p_1,c) = (1 - c) \\cdot (p_1 -\\!_{v} p_0) $$$

Lean4

@[simp]
theorem right_vsub_lineMap (p₀ p₁ : P1) (c : k) : p₁ -ᵥ lineMap p₀ p₁ c = (1 - c) • (p₁ -ᵥ p₀) := by
  rw [← lineMap_apply_one_sub, left_vsub_lineMap]

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