map_sub — Mathlib

English

Let f be a linear partial map from E to F. Then f preserves subtraction: for all x, y in the domain of f, f(x − y) = f(x) − f(y).

Русский

Пусть f — линейное частичное отображение из E в F. Тогда оно сохраняет вычитание: для всех x, y из области определения f выполняется f(x − y) = f(x) − f(y).

LaTeX

$$$\\forall f:\\,E\\to\\!_{R}F\\,\\;\\forall x,y\\in\\mathrm{dom}(f):\\; f(x-y)=f(x)-f(y)$$$

Lean4

theorem map_sub (f : E →ₗ.[R] F) (x y : f.domain) : f (x - y) = f x - f y :=
  f.toFun.map_sub x y

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