map_add

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.map_add

English

Let e be a continuous linear equivalence. Then e preserves addition: e(x+y) = e(x) + e(y).

Русский

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

LaTeX

$$$e(x+y) = e(x) + e(y)$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru