sub_linear — Mathlib

English

Affine maps from P1 to V2 form an affine space over the vector-space valued affine maps from P1 to P2, with vadd defined pointwise.

Русский

Аффинные отображения образуют аффинное пространство над пространством векторных отображений, действием по точкам определяемым по точкам.

LaTeX

$$$\mathrm{Aff}_k(P_1,V_2) \text{ is an affine space over } \mathrm{Aff}_k(P_1,P_2) \text{ with } vadd$ defined pointwise.$$

Lean4

@[simp]
theorem sub_linear (f g : P1 →ᵃ[k] V2) : (f - g).linear = f.linear - g.linear :=
  rfl

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