mdifferentiableAt_symm

Mathlib.Geometry.Manifold.MFDeriv.Atlas

URI: https://scilib.ai/kg/mathlib#OpenPartialHomeomorph.MDifferentiable.mdifferentiableAt_symm

← MathLib Explorer

English

For x in M', the derivative of e.symm at x exists: MDifferentiableAt I' I e.symm x.

Русский

Для x в M' существует производная отображения e.symm в точке x: MDifferentiableAt I' I e.symm x.

LaTeX

$$$\mathrm{MDifferentiableAt}(I',I, e^{\mathrm{symm}}, x)$$$

Lean4

theorem mdifferentiableAt_symm {x : M'} (hx : x ∈ e.target) : MDifferentiableAt I' I e.symm x :=
  (he.2 x hx).mdifferentiableAt (e.open_target.mem_nhds hx)

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

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

Разделы

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

Аффилиация

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