map_sub — Mathlib

English

Let e be a continuous linear equivalence. Then e(x − y) = ex − ey, i.e., e is additive over subtraction.

Русский

Пусть e — непрерывное линейное эквивалентное отображение. Тогда e(x − y) = ex − ey, то есть e сохраняет вычитание.

LaTeX

$$$e(x - y) = e x - e y$$$

Lean4

theorem map_sub (e : M ≃SL[σ₁₂] M₂) (x y : M) : e (x - y) = e x - e y :=
  (e : M →SL[σ₁₂] M₂).map_sub x y

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