homothety_add — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem homothety_add (c : P1) (r₁ r₂ : k) : homothety c (r₁ + r₂) = r₁ • (id k P1 -ᵥ const k P1 c) +ᵥ homothety c r₂ :=
  by simp only [homothety_def, add_smul, vadd_vadd]

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