English
If f is differentiable on s, then f − g is differentiable on s iff g is differentiable on s.
Русский
Если f дифференцируема на s, то f − g дифференцируема на s тогда же, что и g.
LaTeX
$$$\\text{DifferentiableOn}_{\\mathbb{k}}(f, s) \\Rightarrow \\left(\\text{DifferentiableOn}_{\\mathbb{k}}(f - g, s) \\iff \\text{DifferentiableOn}_{\\mathbb{k}}(g, s)\\right)$$$
Lean4
@[simp]
theorem fun_sub_iff_right (hg : DifferentiableOn 𝕜 f s) :
DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g s := by
simp only [sub_eq_add_neg, differentiableOn_fun_neg_iff, hg, fun_add_iff_right]