hasMFDerivAt — Mathlib

English

A Continuous Linear Equivalence has MF-derivative at x equal to its underlying linear map.

Русский

Непрерывно линейное эквивалентное отображение имеет MF-производную в точке x, равную своему линейному отображению.

LaTeX

$$HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') (EquivLike.toFunLike.coe f) x (f.toContinuousLinearMap)$$

Lean4

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

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