vsub_toAffineMap — Mathlib

English

For f: P →ᴬ[R] W and g: P →ᴬ[R] Q, the underlying affine map of their difference by vsub equals the difference of their underlying affine maps: (f -ᵥ g).toAffineMap = f.toAffineMap -ᵥ g.toAffineMap.

Русский

Для f: P →ᴬ[R] W и g: P →ᴬ[R] Q вершинное отображение разности (f -ᵥ g).toAffineMap равно f.toAffineMap -ᵥ g.toAffineMap.

LaTeX

$$$$(f -\\!_v g).toAffineMap = f.toAffineMap -\\!_v g.toAffineMap.$$$$

Lean4

@[simp]
theorem vsub_toAffineMap (f g : P →ᴬ[R] Q) : (f -ᵥ g).toAffineMap = f.toAffineMap -ᵥ g.toAffineMap :=
  rfl

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