hasGradientAt — Mathlib

English

From HasDerivAt g g' u we get HasGradientAt g (starRingEnd 𝕜 g') u.

Русский

Производная в точке универсального поля имплицитно задаёт градиент через сопряжение.

LaTeX

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

Lean4

theorem hasGradientAt (h : HasDerivAt g g' u) : HasGradientAt g (starRingEnd 𝕜 g') u :=
  by
  rw [hasGradientAt_iff_hasFDerivAt, hasFDerivAt_iff_hasDerivAt]
  simpa

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