fun_sub_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_sub_iff_right (hg : Differentiable 𝕜 f) : Differentiable 𝕜 (fun y => f y - g y) ↔ Differentiable 𝕜 g := by
  simp only [sub_eq_add_neg, differentiable_fun_neg_iff, hg, fun_add_iff_right]

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