fun_add_iff_left — Mathlib

English

If g is differentiable on s, then f + g is differentiable on s iff f is differentiable on s.

Русский

Если g дифференцируема на s, то f + g дифференцируема на s тогда же, что и f.

LaTeX

$$$\\text{DifferentiableOn}_{\\mathbb{k}}(f + g , s) \\iff \\text{DifferentiableOn}_{\\mathbb{k}}(f, s)$ (given $\\text{DifferentiableOn}_{\\mathbb{k}}(g, s)$)$$

Lean4

@[simp]
theorem fun_add_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 f s :=
  by
  refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩
  simpa only [add_sub_cancel_right] using h.fun_sub hg

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