hasGradientAt_iff_hasFDerivAt

Mathlib.Analysis.Calculus.Gradient.Basic

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

English

The HasGradientAt relation between f, f' and x encodes differentiability of f at x with gradient f'.

Русский

Отношение HasGradientAt между f, f' и x кодирует дифференцируемость f в x с градиентом f'.

LaTeX

$$$ HasGradientAt f f' x $$$

Lean4

theorem hasGradientAt_iff_hasFDerivAt : HasGradientAt f f' x ↔ HasFDerivAt f (toDual 𝕜 F f') x :=
  Iff.rfl

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

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

Разделы

Аффилиация

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