English
Let f and g be differentiable within a set s at x. Then the derivative within s of f − g at x equals the derivative within s of f at x minus the derivative within s of g at x.
Русский
Пусть функции f и g дифференцируемы внутри множества s в точке x. Тогда производная внутри s от f − g в x равна разности производных: производная f внутри s в x minus производная g внутри s в x.
LaTeX
$$$$ \operatorname{derivWithin}(f - g) \ s \ x = \operatorname{derivWithin} f \ s \ x - \operatorname{derivWithin} g \ s \ x. $$$$
Lean4
theorem derivWithin_fun_sub (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
simp only [sub_eq_add_neg, derivWithin_fun_add hf hg.fun_neg, derivWithin.fun_neg]
