differentiableWithinAt — Mathlib

English

If HasGradientWithinAt f f' s x holds, then f is differentiableWithinAt 𝕜 f s x.

Русский

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

LaTeX

$$$\\text{HasGradientWithinAt } f f' s x \\Rightarrow \\text{DifferentiableWithinAt } 𝕜 f s x$$$

Lean4

theorem differentiableWithinAt (h : HasGradientWithinAt f f' s x) : DifferentiableWithinAt 𝕜 f s x :=
  h.hasFDerivWithinAt.differentiableWithinAt

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