sub — Mathlib

English

If hf and hg are HasStrictFDerivAt f f′ x and g g′ x, then HasStrictFDerivAt (f − g) (f′ − g′) x.

Русский

Если hf и hg являются строгими производными HasStrictFDerivAt f f′ x и HasStrictFDerivAt g g′ x, то HasStrictFDerivAt (f − g) (f′ − g′) x.

LaTeX

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

Lean4

@[fun_prop]
theorem sub (hf : HasStrictFDerivAt f f' x) (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (f - g) (f' - g') x :=
  hf.fun_sub hg

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