sub — Mathlib

English

If hf : HasFDerivWithinAt f f' s x and hg : HasFDerivWithinAt g g' s x, then HasFDerivWithinAt (fun x => f x − g x) (f' − g') s x.

Русский

Если hf : HasFDerivWithinAt f f' s x и hg : HasFDerivWithinAt g g' s x, тогда HasFDerivWithinAt (fun x => f x − g x) (f' − g') s x.

LaTeX

$$HasFDerivWithinAt (f − g) (f′ − g′) s x$$

Lean4

@[fun_prop]
nonrec theorem sub (hf : HasFDerivWithinAt f f' s x) (hg : HasFDerivWithinAt g g' s x) :
    HasFDerivWithinAt (f - g) (f' - g') s x :=
  hf.sub hg

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