English
Let f and g be maps from a charted space M to a normed space E'. If both f and g are differentiable in the MF-derivative sense, then their sum f + g is differentiable in the same sense.
Русский
Пусть f и g — отображения из чарта пространства M в нормированное пространство E'. Если оба отображения дифференцируемы в смысле MF-дифференцируемости, то сумма f + g также дифференцируема в этом смысле.
LaTeX
$$$\forall f,g: M \to E',\; MDifferentiable I \; \mathcal{I}(\kappa, E')\, f \wedge MDifferentiable I \, \mathcal{I}(\kappa, E')\, g \Rightarrow MDifferentiable I \, \mathcal{I}(\kappa, E')\, (f+g).$$$
Lean4
theorem add (hf : MDifferentiable I 𝓘(𝕜, E') f) (hg : MDifferentiable I 𝓘(𝕜, E') g) :
MDifferentiable I 𝓘(𝕜, E') (f + g) := fun x =>
(hf x).add
(hg x)
-- Porting note: forcing types using `by exact`
