lineMap_vsub_right — Mathlib

English

With the same data, the displacement from lineMap(p0, p1, c) to p1 is (1 − c) times the displacement from p0 to p1, i.e., lineMap(p0,p1,c) − p1 = (1 − c) · (p0 − p1).

Русский

Величина vsub между lineMap(p0,p1,c) и p1 равна (1 − c) раза вектора от p0 к p1: lineMap(p0,p1,c) − p1 = (1 − c) · (p0 − p1).

LaTeX

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

Lean4

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

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