vadd_lineMap — Mathlib

English

Let k be a ring and P1 a nonempty affine space modeled on V1. For any vector v in V1, any points p1, p2 in P1, and any scalar c in k, translating the entire configuration by v sends lineMap(p1, p2)(c) to lineMap(v + p1, v + p2)(c).

Русский

Пусть k — кольцо, P1 — аффинное пространство над V1. Для любого вектора v ∈ V1, точек p1, p2 ∈ P1 и скаляра c ∈ k перенос всей конфигурации на v переводит lineMap(p1, p2)(c) в lineMap(v + p1, v + p2)(c).

LaTeX

$$$ v +\!\,\mathrm{lineMap}(p_1,p_2)(c) = \mathrm{lineMap}(v+\!\,p_1)(v+\!\,p_2)(c) $$$

Lean4

theorem vadd_lineMap (v : V₁) (p₁ p₂ : P₁) (c : k) : v +ᵥ lineMap p₁ p₂ c = lineMap (v +ᵥ p₁) (v +ᵥ p₂) c :=
  (constVAdd k P₁ v).apply_lineMap p₁ p₂ c

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