HasDerivAtFilter — Mathlib

English

The derivative within a set s at x, denoted derivWithin f s x, is defined by fderivWithin 𝕜 f s x 1; it gives the slope of f restricted near x inside s.

Русский

Производная внутри множества s в точке x задается через fderivWithin 𝕜 f s x 1 и дает касательную к f внутри s около x.

LaTeX

$$$\\mathrm{derivWithin}(f, s, x) := fderivWithin\\; 𝕜\\; f\\; s\\; x\\; 1$$$

Lean4

/-- `f` has the derivative `f'` at the point `x` as `x` goes along the filter `L`.

That is, `f x' = f x + (x' - x) • f' + o(x' - x)` where `x'` converges along the filter `L`.
-/
def HasDerivAtFilter (f : 𝕜 → F) (f' : F) (x : 𝕜) (L : Filter 𝕜) :=
  HasFDerivAtFilter f (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') x L

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