localInverse_apply_image

Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff

URI: https://scilib.ai/kg/mathlib#ContDiffAt.localInverse_apply_image

← MathLib Explorer

English

Applying the local inverse to f(a) yields a.

Русский

Применяя локальную обратную к f(a), получаем a.

LaTeX

$$$\text{ContDiffAt }.localInverse (f a) = a$$$

Lean4

theorem localInverse_apply_image (hf : ContDiffAt 𝕂 n f a) (hf' : HasFDerivAt f (f' : E →L[𝕂] F) a) (hn : 1 ≤ n) :
    hf.localInverse hf' hn (f a) = a :=
  (hf.hasStrictFDerivAt' hf' hn).localInverse_apply_image

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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