hasGradientWithinAt — Mathlib

English

If f is differentiable within s at x, then the gradient within s at x exists and equals gradientWithin f s x.

Русский

Если функция f дифференцируема внутри множества s в точке x, то градиент внутри s в x существует и равен gradientWithin f s x.

LaTeX

$$$\\text{DifferentiableWithinAt } 𝕜\\ f\\ s\\ x \\Rightarrow \\text{HasGradientWithinAt } f (\\nabla f\\ s\\ x)\\ s\\ x$$$

Lean4

theorem hasGradientWithinAt (h : DifferentiableWithinAt 𝕜 f s x) : HasGradientWithinAt f (gradientWithin f s x) s x :=
  by
  rw [hasGradientWithinAt_iff_hasFDerivWithinAt, gradientWithin, (toDual 𝕜 F).apply_symm_apply (fderivWithin 𝕜 f s x)]
  exact h.hasFDerivWithinAt

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