map_sub_right

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

URI: https://scilib.ai/kg/mathlib#IsBoundedBilinearMap.map_sub_right

← MathLib Explorer

English

For a bilinear map f, f(x, y - z) = f(x, y) - f(x, z).

Русский

Для билинейного отображения f выполняется f(x, y - z) = f(x, y) - f(x, z).

LaTeX

$$$f( x, y - z) = f(x, y) - f(x, z)$$$

Lean4

theorem map_sub_right (h : IsBoundedBilinearMap 𝕜 f) {x : E} {y z : F} : f (x, y - z) = f (x, y) - f (x, z) :=
  (h.toContinuousLinearMap x).map_sub y z

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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