hasFDerivAtFilter — Mathlib

English

If f is Fréchet differentiable at x with derivative f', then for any filter L with L ≤ 𝓝 x, f is Fréchet differentiable along L with derivative f'.

Русский

Если f имеет производную Фреше в точке x с производной f', то для любого фильтра L, удовлетворяющего L ≤ 𝓝 x, производна вдоль L существует с той же производной.

LaTeX

$$$$\\text{HasFDerivAt } f\\,f'\\,x \\implies \\text{HasFDerivAtFilter } f\\,f'\\,x\\,L \\text{ for all } L \\le 𝓝 x.$$$$

Lean4

theorem hasFDerivAtFilter (h : HasFDerivAt f f' x) (hL : L ≤ 𝓝 x) : HasFDerivAtFilter f f' x L :=
  h.mono hL

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