differentiableAt — Mathlib

English

If a function f has a gradient f′ at a point x, then f is differentiable at x (Fréchet differentiable) and the derivative is given by the linear map h ↦ ⟪f′, h⟫.

Русский

Если функция f имеет градиент f′ в точке x, то f дифференцируема в точке x (фрешевая дифференцируемость), и производная задаётся линейным отображением h ↦ ⟪f′, h⟫.

LaTeX

$$$\\text{HasGradientAt}(f,f',x) \\Rightarrow \\text{DifferentiableAt } 𝕜\\ f\\ x$$$

Lean4

theorem differentiableAt (h : HasGradientAt f f' x) : DifferentiableAt 𝕜 f x :=
  h.hasFDerivAt.differentiableAt

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