derivWithin — Mathlib

English

Within any set s, the derivative of the linear map e is e(1) at any point x ∈ dom, provided the usual differentiability holds inside s.

Русский

Внутри любой области s производная линейного отображения e равна e(1) в любой точке x, где выполняется обычная дифференцируемость внутри s.

LaTeX

$$$\\operatorname{derivWithin}(e,\;s,\;x) = e(1)$$$

Lean4

protected theorem derivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) : derivWithin e s x = e 1 :=
  e.hasDerivWithinAt.derivWithin hxs

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