mdifferentiableAt — Mathlib

English

The MF-derivative of a Continuous Linear Equivalence at x is its underlying linear map.

Русский

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

LaTeX

$$mfderiv 𝓘(𝕜, E) 𝓘(𝕜, E') (EquivLike.toFunLike.coe f) x = (f : E →L[𝕜] E')$$

Lean4

protected theorem mdifferentiableAt : MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x :=
  f.differentiableAt.mdifferentiableAt

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