contMDiffOn_chart_symm

Mathlib.Geometry.Manifold.ContMDiff.Atlas

URI: https://scilib.ai/kg/mathlib#contMDiffOn_chart_symm

← MathLib Explorer

English

The inverse extChartAt is smooth of order n on its range.

Русский

Обратная extChartAt гладна порядка n на своем диапазоне.

LaTeX

$$$\mathrm{ContMDiffOn}\, (\mathrm{extChartAt}\ I\ x)^{-1} :\mathrm{range} \ I \to \mathrm{domain}$$$

Lean4

theorem contMDiffOn_chart_symm : ContMDiffOn I I n (chartAt H x).symm (chartAt H x).target :=
  contMDiffOn_symm_of_mem_maximalAtlas <| chart_mem_maximalAtlas x

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

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

Разделы

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

Аффилиация

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