coe_coe''

Mathlib.Analysis.Normed.Operator.LinearIsometry

URI: https://scilib.ai/kg/mathlib#LinearIsometryEquiv.coe_coe''

English

A linear isometry preserves addition: e(x+y) = ex + ey.

Русский

Линейная изометрия сохраняет сложение: e(x+y) = e(x) + e(y).

LaTeX

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

Lean4

@[simp]
theorem coe_coe'' : ⇑(e : E →SL[σ₁₂] E₂) = e :=
  rfl

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

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

Разделы

Аффилиация

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