instSub — Mathlib

English

There is a subtraction 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 : Sub (P1 →ᵃ[k] V2) where sub f g := ⟨f - g, f.linear - g.linear, fun p v => by simp [sub_add_sub_comm]⟩

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