hasDerivAt'

Mathlib.Analysis.Calculus.Gradient.Basic

URI: https://scilib.ai/kg/mathlib#HasGradientAt.hasDerivAt'

English

HasDerivAt hasGradientAt: HasDerivAt g g' u implies HasGradientAt g g' u (via starRingEnd).

Русский

Производная в точке u определяет градиент через сопряжение.

LaTeX

$$$\\text{HasDerivAt } g g' u \\Rightarrow \\text{HasGradientAt } g (\\starRingEnd 𝕜\\ g') u$$$

Lean4

theorem hasDerivAt' (h : HasGradientAt g g' u) : HasDerivAt g g' u :=
  h.hasDerivAt

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

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

Разделы

Аффилиация

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