Theorems · Definition · global analysis

HasGradientWithinAt

{𝕜 : Type u_1} →
  {F : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup F] → [InnerProductSpace 𝕜 F] → [CompleteSpace F] → (F → 𝕜) → F → Set F → F → Prop

f has the gradient f' at the point x within the subset s if f x' = f x + ⟨f', x' - x⟩ + o (x' - x) where x' converges to x inside s.

Defined in

Mathlib.Analysis.Calculus.Gradient.Basic

Cited by

20 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceCompleteSpace