contMDiffOn_chart

Mathlib.Geometry.Manifold.ContMDiff.Atlas

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

English

The symmetric of a chart, extended appropriately, is C^n-smooth on its target.

Русский

Симметричная карта чартa, при надлежащем расширении, гладна по порядку n на своей цели.

LaTeX

$$$\mathrm{ContMDiffOn}(I, I, n, e.symm, e.target)$$$

Lean4

theorem contMDiffOn_chart : ContMDiffOn I I n (chartAt H x) (chartAt H x).source :=
  contMDiffOn_of_mem_maximalAtlas <| chart_mem_maximalAtlas x

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

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

Разделы

Аффилиация

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