HasDerivWithinAt — Mathlib

English

There exists a slope f' such that f is differentiable at x with that slope; i.e., HasDerivAt f f' x.

Русский

Существует касательная скорость f' такая, что f дифференцируема в точке x с этой скоростью.

LaTeX

$$$\\text{HasDerivAt}(f,f',x).$$$

Lean4

/-- `f` has the derivative `f'` at the point `x` within the subset `s`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges to `x` inside `s`.
-/
def HasDerivWithinAt (f : 𝕜 → F) (f' : F) (s : Set 𝕜) (x : 𝕜) :=
  HasDerivAtFilter f f' x (𝓝[s] x)

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