English
If f and g have MF-derivatives at a point, then f+g has MF-derivative at that point, equal to the sum of the derivatives.
Русский
Если у функций f и g есть MF-производные в точке, то f+g имеет MF-производную в этой точке, равную сумме производных.
LaTeX
$$$\text{HasMFDerivAt } I\ 𝓘(\mathbb{K},E')\ f x f' \land \text{HasMFDerivAt } I\ 𝓘(\mathbb{K},E')\ g x g' \Rightarrow \text{HasMFDerivAt } I\ 𝓘(\mathbb{K},E')\ (f+g) x (f'+g')$$$
Lean4
/-- The total derivative of a function in two variables is the sum of the partial derivatives.
Note that to state this (without casts) we need to be able to see through the definition of
`TangentSpace`. Version in terms of the one-variable derivatives. -/
theorem mfderiv_prod_eq_add_apply {f : M × M' → M''} {p : M × M'} {v : TangentSpace (I.prod I') p}
(hf : MDifferentiableAt (I.prod I') I'' f p) :
mfderiv (I.prod I') I'' f p v =
mfderiv I I'' (fun z : M => f (z, p.2)) p.1 v.1 + mfderiv I' I'' (fun z : M' => f (p.1, z)) p.2 v.2 :=
by
rw [mfderiv_prod_eq_add_comp hf]
rfl
