combo_affine_apply — Mathlib

English

Applying an affine map to an affine combination of two points yields the corresponding affine combination of the images.

Русский

Применение аффинного отображения к аффинной комбинации двух точек даёт соответствующую аффинную комбинацию изображений.

LaTeX

$$f(a x + b y) = a f(x) + b f(y) при a + b = 1$$

Lean4

/-- Applying an affine map to an affine combination of two points yields an affine combination of
the images. -/
theorem combo_affine_apply {x y : E} {a b : 𝕜} {f : E →ᵃ[𝕜] F} (h : a + b = 1) :
    f (a • x + b • y) = a • f x + b • f y :=
  by
  simp only [Convex.combo_eq_smul_sub_add h, ← vsub_eq_sub]
  exact f.apply_lineMap _ _ _

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