add_iff_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add_iff_left (hg : Differentiable 𝕜 g) : Differentiable 𝕜 (f + g) ↔ Differentiable 𝕜 f :=
  hg.fun_add_iff_left

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