hasMFDerivAt — Mathlib

English

For a continuous linear map f, the MF-derivative within at x is f at every x (on any subset).

Русский

Для непрерывно линейного отображения f MF-производная внутри в точке равна f (на любом подмножестве).

LaTeX

$$HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x$$

Lean4

protected theorem hasMFDerivAt : HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f :=
  f.hasFDerivAt.hasMFDerivAt

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