English
If f and g are differentiable at a point with MF-derivative, then the MF-derivative of f + g at that point equals the sum of MF-derivatives of f and g at that point.
Русский
Если в точке f и g дифференциируемы в MF-деривативном смысле, то производная mfderiv(f+g) равна сумме производных mfderiv(f) + mfderiv(g) в этой точке.
LaTeX
$$$\forall z:\, z\in M,\; MDifferentiableAt I\, 𝓘(𝕜,E')\, f\, z\wedge MDifferentiableAt I\, 𝓘(𝕜,E')\, g\, z \Rightarrow mfderiv I 𝓘(𝕜,E')(f+g) z = mfderiv I 𝓘(𝕜,E') f z + mfderiv I 𝓘(𝕜,E') g z.$$$
Lean4
theorem mfderiv_add (hf : MDifferentiableAt I 𝓘(𝕜, E') f z) (hg : MDifferentiableAt I 𝓘(𝕜, E') g z) :
(by exact mfderiv I 𝓘(𝕜, E') (f + g) z : TangentSpace I z →L[𝕜] E') =
(by exact mfderiv I 𝓘(𝕜, E') f z) + (by exact mfderiv I 𝓘(𝕜, E') g z) :=
(hf.hasMFDerivAt.add hg.hasMFDerivAt).mfderiv
