fun_sub_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}}(g, s) \\Rightarrow \\left(\\text{DifferentiableOn}_{\\mathbb{k}}(f - g, s) \\iff \\text{DifferentiableOn}_{\\mathbb{k}}(f, s)\\right)$$$

Lean4

@[simp]
theorem fun_sub_iff_left (hg : DifferentiableOn 𝕜 g s) :
    DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 f s := by
  simp only [sub_eq_add_neg, differentiableOn_fun_neg_iff, hg, fun_add_iff_left]

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