hasMFDerivWithinAt

Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.hasMFDerivWithinAt

English

The MF-derivative of a continuous linear map at any point equals that map itself.

Русский

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

LaTeX

$$HasMFDerivAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x f$$

Lean4

protected theorem hasMFDerivWithinAt : HasMFDerivWithinAt 𝓘(𝕜, E) 𝓘(𝕜, E') f s x f :=
  f.hasFDerivWithinAt.hasMFDerivWithinAt

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru