derivWithin — Mathlib

English

Let f be an affine map 𝕜 →ᵃ[𝕜] E. If the derivative within a set s exists at x (UniqueDiffWithinAt 𝕜 s x), then its derivative equals the linear part evaluated at 1, i.e. derivWithin f s x = f.linear 1.

Русский

Пусть f — аффинное отображение 𝕜 →ᵃ[𝕜] E. Если в точке x внутри множества s существует производная внутри области (UniqueDiffWithinAt 𝕜 s x), то её значение равно линейной части f, применённой к 1: derivWithin f s x = f.linear 1.

LaTeX

$$$\\operatorname{derivWithin}(f,s,x) = f_{\\text{linear}}(1).$$$

Lean4

protected theorem derivWithin (hs : UniqueDiffWithinAt 𝕜 s x) : derivWithin f s x = f.linear 1 :=
  f.hasDerivWithinAt.derivWithin hs

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