left_vsub_lineMap — Mathlib

English

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

Русский

При тех же предпосылках вектор vsub от p0 к lineMap(p0, p1, c) равен c умноженному на вектор от p1 к p0: p0 − lineMap(p0, p1, c) = c · (p0 − p1).

LaTeX

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

Lean4

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

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