derivWithin — Mathlib

English

For q ∈ Polynomial R, x ∈ 𝕜 and s, the derivative within s of x ↦ aeval x q equals aeval x (derivative q).

Русский

Для q ∈ Polynomial R, x ∈ 𝕜 и s, производная внутри s от x ↦ aeval x q равна aeval x (derivative q).

LaTeX

$$$derivWithin\_\{\mathbb{K}\}\left(\lambda x, aeval x q\right) s x = aeval x (derivative q)$$$

Lean4

protected theorem derivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
    derivWithin (fun x => p.eval x) s x = p.derivative.eval x :=
  by
  rw [DifferentiableAt.derivWithin p.differentiableAt hxs]
  exact p.deriv

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