map_sub₂

Mathlib.Analysis.Normed.Operator.BoundedLinearMaps

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.map_sub₂

English

The map f on (x - x') equals f(x) - f(x') for bilinear maps.

Русский

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

LaTeX

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

Lean4

theorem map_sub₂ (f : M →SL[ρ₁₂] F →SL[σ₁₂] G') (x x' : M) (y : F) : f (x - x') y = f x y - f x' y := by
  rw [f.map_sub, sub_apply]

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

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

Разделы

Аффилиация

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