fun_add_iff_right — Mathlib

English

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

Русский

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

LaTeX

$$$\\text{Differentiable}(f) \\Rightarrow \\left(\\text{Differentiable}(f + g) \\iff \\text{Differentiable}(g)\\right)$$$

Lean4

@[simp]
theorem fun_add_iff_right (hg : Differentiable 𝕜 f) : Differentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 g := by
  simp only [add_comm (f _), hg.fun_add_iff_left]

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