fun_sub_iff_right — Mathlib

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]

Похожие утверждения