map_sub_left — Mathlib

English

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

Русский

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

LaTeX

$$$f(\{ fst := x, snd := -y \}, z) = f(\{ fst := x, snd := z \},) - f(\{ fst := y, snd := z \},)$$$

Lean4

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

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