map_zero

Mathlib.Analysis.Normed.Operator.LinearIsometry

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

English

A linear isometry preserves subtraction: e(x - y) = e(x) - e(y).

Русский

Линейная изометрия сохраняет вычитание: e(x - y) = e(x) - e(y).

LaTeX

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

Lean4

theorem map_zero : e 0 = 0 :=
  e.1.map_zero

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

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

Разделы

Аффилиация

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