English
If f,g are differentiable within s at x, then the derivative within s of f + g is the sum of their derivatives within s.
Русский
Если f и g дифференцируемы внутри s в x, то производная внутри s от f + g равна сумме производных внутри s.
LaTeX
$$$\text{DifferentiableWithinAt } f s x \land \text{DifferentiableWithinAt } g s x \Rightarrow \ derivWithin (f + g) s x = derivWithin f s x + derivWithin g s x$$$
Lean4
theorem derivWithin_fun_add (hf : DifferentiableWithinAt 𝕜 f s x) (hg : DifferentiableWithinAt 𝕜 g s x) :
derivWithin (fun y ↦ f y + g y) s x = derivWithin f s x + derivWithin g s x :=
by
by_cases hsx : UniqueDiffWithinAt 𝕜 s x
· exact (hf.hasDerivWithinAt.add hg.hasDerivWithinAt).derivWithin hsx
· simp [derivWithin_zero_of_not_uniqueDiffWithinAt hsx]
