Theorems · Theorem · global analysis

HasDerivAtFilter.hasGradientAtFilter

∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {g : 𝕜 → 𝕜} {g' u : 𝕜} {L' : Filter 𝕜},
  HasDerivAtFilter g g' (L' ×ˢ pure u) → HasGradientAtFilter g ((starRingEnd 𝕜) g') u L'

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

1 results in Mathlib

Foundations

Depth 186 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLike