fderivWithin_fun_sub — Mathlib

English

The derivative within a set of the difference is the difference of derivatives within the set.

Русский

Дифференциал внутри множества функции разности равен разности дифференциалов внутри множества.

LaTeX

$$$\\text{fderivWithin}_{\\mathbb{k}} (f - g) \\text{within } s = \\text{fderivWithin}_{\\mathbb{k}} f \\text{within } s - \\text{fderivWithin}_{\\mathbb{k}} g \\text{within } s$$$

Lean4

theorem fderivWithin_fun_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) :
    fderivWithin 𝕜 (fun y => f y - g y) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x :=
  (hf.hasFDerivWithinAt.sub hg.hasFDerivWithinAt).fderivWithin hxs

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