HasGradientWithinAt — Mathlib

English

HasGradientWithinAt f f' s x means that the gradient of f at x inside s is f'.

Русский

HasGradientWithinAt f f' s x означает, что градиент f в точке x внутри множества s равен f'.

LaTeX

$$$ HasGradientWithinAt f f' s x $$$

Lean4

/-- `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`. -/
def HasGradientWithinAt (f : F → 𝕜) (f' : F) (s : Set F) (x : F) :=
  HasGradientAtFilter f f' x (𝓝[s] x)

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