fderivWithin_sub — Mathlib

English

The formula for fderivWithin of a difference holds: fderivWithin (f − g) = fderivWithin f − fderivWithin g.

Русский

Формула для fderivWithin разности: fderivWithin(...)=fderivWithin f − fderivWithin g.

LaTeX

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

Lean4

theorem fderivWithin_sub (hxs : UniqueDiffWithinAt 𝕜 s x) (hf : DifferentiableWithinAt 𝕜 f s x)
    (hg : DifferentiableWithinAt 𝕜 g s x) : fderivWithin 𝕜 (f - g) s x = fderivWithin 𝕜 f s x - fderivWithin 𝕜 g s x :=
  fderivWithin_fun_sub hxs hf hg

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