map_vadd — Mathlib

English

For an affine equivalence e: P1 ≃ᵃ[k] P², a base point p ∈ P1 and a vector v ∈ V1, the image of p translated by v equals the image of p translated by the linear part of e: e(v + p) = e.linear(v) + e(p).

Русский

Для аффинного эквивалентного отображения e: P1 ≃ᵃ[k] P2, базовой точки p ∈ P1 и вектора v ∈ V1 изображение p, смещенного на v, равно изображению p, смещенному линейной частью e: e(v + p) = e.linear(v) + e(p).

LaTeX

$$$e(v\,+\_v p) = (e.linear)\,v \,+\_v e(p)$$$

Lean4

@[simp]
theorem map_vadd (e : P₁ ≃ᵃ[k] P₂) (p : P₁) (v : V₁) : e (v +ᵥ p) = e.linear v +ᵥ e p :=
  e.map_vadd' p v

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