hasFDerivAtFilter — Mathlib

English

If e is a linear map between normed spaces, then it has a Fréchet derivative at every point with derivative e, and in particular has a derivative in the filter sense along any filter L.

Русский

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

LaTeX

$$$$ HasFDerivAt e e x \\quad\\text{for all } x, \\text{ and } HasFDerivAtFilter e e x L. $$$$

Lean4

protected theorem hasFDerivAtFilter : HasFDerivAtFilter e e x L :=
  .of_isLittleOTVS <| (IsLittleOTVS.zero _ _).congr_left fun x => by simp only [e.map_sub, sub_self, Pi.zero_apply]

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