contMDiffWithinAt_extChartAt_symm_target

Mathlib.Geometry.Manifold.ContMDiff.Atlas

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

← MathLib Explorer

English

The extChartAt map is C^n-smooth at x.

Русский

extChartAt гладна порядка n в точке x.

LaTeX

$$$\mathrm{ContMDiffAt}\; I\; (\mathrm{extChartAt}\ I x) x$$$

Lean4

theorem contMDiffWithinAt_extChartAt_symm_target (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target y :=
  contMDiffOn_extChartAt_symm x y hy

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

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

Разделы

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

Аффилиация

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