lineMap_vsub_left — Mathlib

English

Let k be a field, V1 an additive abelian group with a k-module structure, and P1 an affine space modeled on V1. For any p0, p1 in P1 and any c in k, the displacement from p0 to the point lineMap(p0, p1, c) equals c times the displacement from p0 to p1.

Русский

Пусть k — поле, V1 — абелева группа с модулем над k, P1 — аффинное пространство, моделируемое по V1. Для любых p0, p1 ∈ P1 и любого c ∈ k вектор от p0 к точке lineMap(p0, p1, c) равен скалярному умножению c на вектор p1 относительно p0: lineMap(p0, p1, c) − p0 = c · (p1 − p0).

LaTeX

$$$ lineMap(p_0,p_1,c) - p_0 = c \\cdot (p_1 - p_0) $$$

Lean4

@[simp]
theorem lineMap_vsub_left (p₀ p₁ : P1) (c : k) : lineMap p₀ p₁ c -ᵥ p₀ = c • (p₁ -ᵥ p₀) :=
  vadd_vsub _ _

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