instAdd — Mathlib

English

There is a natural addition on affine maps: f + g is defined by (f + g)(p) = f(p) + g(p) and (f + g).linear = f.linear + g.linear.

Русский

Существует естественное сложение аффинных отображений: (f + g)(p) = f(p) + g(p) и (f + g).linear = f.linear + g.linear.

LaTeX

$$$\forall f,g:\, P_1 \to^{\mathrm{aff}}_k V_2,\ (f+g)_{\mathrm{linear}} = f_{\mathrm{linear}} + g_{\mathrm{linear}}$$$

Lean4

instance : Add (P1 →ᵃ[k] V2) where add f g := ⟨f + g, f.linear + g.linear, fun p v => by simp [add_add_add_comm]⟩

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