mdifferentiableWithinAt — Mathlib

English

The MF-derivative within for a continuous linear equivalence equals its derivative map.

Русский

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

LaTeX

$$HasMFDerivWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') (EquivLike.toFunLike.coe f) s x (f.toContinuousLinearMap)$$

Lean4

protected theorem mdifferentiableWithinAt : MDifferentiableWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x :=
  f.differentiableWithinAt.mdifferentiableWithinAt

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