fun_sub — Mathlib

English

If f and g have strict derivatives f′ and g′ at x, then the function x ↦ f(x) − g(x) has strict derivative f′ − g′ at x.

Русский

Если у функций f и g в точке x существуют строгие производные f′ и g′, то функция x ↦ f(x) − g(x) имеет строгое производное f′ − g′ в x.

LaTeX

$$HasStrictFDerivAt (f − g) (f′ − g′) x$$

Lean4

@[fun_prop]
theorem fun_sub (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) :
    HasStrictFDerivAt (fun x => f x - g x) (f' - g') x := by simpa only [sub_eq_add_neg] using hf.add hg.neg

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