apply_lineMap — Mathlib

English

An affine equivalence preserves affine combinations along lines: it maps line parameterizations lineMap(a,b,c) to lineMap(e(a), e(b), c).

Русский

Аффинное эквивалентное отображение сохраняет аффинные сочетания по линиям: отображает lineMap(a,b,c) в lineMap(e(a), e(b), c).

LaTeX

$$$e(\mathrm{LineMap}(a,b,c)) = \mathrm{LineMap}(e(a), e(b), c) \quad (a,b \in P_1, \; c \in k)$$$

Lean4

@[simp]
theorem apply_lineMap (e : P₁ ≃ᵃ[k] P₂) (a b : P₁) (c : k) :
    e (AffineMap.lineMap a b c) = AffineMap.lineMap (e a) (e b) c :=
  e.toAffineMap.apply_lineMap a b c

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