map_add

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

For any c in R, e(c x) = σ₁₂(c) e(x).

Русский

Для любого скаляра c ∈ R выполняется e(c x) = σ₁₂(c) e(x).

LaTeX

$$$ e(c \cdot x) = \sigma_{12}(c) \cdot e(x) $$$

Lean4

theorem map_add (x y : E) : e (x + y) = e x + e y :=
  e.1.map_add x y

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

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

Разделы

Аффилиация

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