gradient_eq

Mathlib.Analysis.Calculus.Gradient.Basic

URI: https://scilib.ai/kg/mathlib#gradient_eq

English

If for every x we have HasGradientAt f (f' x) x, then ∇ f = f'.

Русский

Если для каждой точки x градиент существует и равен f'(x), то градиент функции совпадает с f'.

LaTeX

$$$\\big(\\forall x,\\ HasGradientAt f (f' x) x\\big) \\Rightarrow \\nabla f = f'$$$

Lean4

theorem gradient_eq {f' : F → F} (h : ∀ x, HasGradientAt f (f' x) x) : ∇ f = f' :=
  funext fun x => (h x).gradient

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru