English
Let f be a map that assigns to each x in E a linear operator f(x) : F → G, and suppose f is linear in x. Then for all x, x' in E and y, y' in F, the value of f at (x+x') applied to (y+y') expands as f(x+x')(y+y') = f(x,y) + f.deriv₂(x,y)(x',y') + f(x',y').
Русский
Пусть f — функция, сопоставляющая каждому x ∈ E линейный оператор f(x): F → G, и пусть f линейна по x. Тогда для любых x, x' ∈ E и y, y' ∈ F выполняется разложение f(x+x')(y+y') = f(x,y) + f.deriv₂(x,y)(x',y') + f(x',y').
LaTeX
$$$ f(x+x')(y+y') = f(x,y) + f\\,.deriv_2(x,y)(x',y') + f(x',y') $$$
Lean4
theorem map_add_add (f : E →L[𝕜] Fₗ →L[𝕜] Gₗ) (x x' : E) (y y' : Fₗ) :
f (x + x') (y + y') = f x y + f.deriv₂ (x, y) (x', y') + f x' y' :=
by
simp only [map_add, add_apply, coe_deriv₂, add_assoc]
abel
