hasFDerivAtFilter — Mathlib

English

A linear continuous map e has a Fréchet derivative at every point with derivative e; i.e., HasFDerivAt e e x holds for all x.

Русский

Линейное непрерывное отображение e имеет Фреше-производную в каждой точке с производной-e; т.е. HasFDerivAt e e x выполняется для всех x.

LaTeX

$$$$ HasFDerivAt e e x \\quad \\text{for all } x. $$$$

Lean4

theorem hasFDerivAtFilter (h : IsBoundedLinearMap 𝕜 f) : HasFDerivAtFilter f h.toContinuousLinearMap x L :=
  h.toContinuousLinearMap.hasFDerivAtFilter

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