sub — Mathlib

English

If f and g have strict derivatives f' and g' at x, then f − g has a strict derivative f' − g' at x.

Русский

Если у f и g есть строгие производные f' и g' в x, то f − g имеет строгую производную f' − g' в x.

LaTeX

$$$ \\text{HasStrictDerivAt}(f - g, f' - g', x)$$$

Lean4

theorem sub (hf : HasStrictDerivAt f f' x) (hg : HasStrictDerivAt g g' x) : HasStrictDerivAt (f - g) (f' - g') x := by
  simpa only [sub_eq_add_neg] using hf.add hg.neg

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