fun_add_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_add_iff_right (hg : DifferentiableOn 𝕜 f s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g s := by
  simp only [add_comm (f _), hg.fun_add_iff_left]

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