contMDiffAt_extend

Mathlib.Geometry.Manifold.ContMDiff.Atlas

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

← MathLib Explorer

English

Chart extension maps are C^n-smooth on their sources.

Русский

Карт-расширения гладны порядка n на исходных областях.

LaTeX

$$$\mathrm{ContMDiffOn}\, (\mathrm{chartAt}\ H x) \text{ on source } x$$$

Lean4

theorem contMDiffAt_extend {x : M} (he : e ∈ maximalAtlas I n M) (hx : x ∈ e.source) :
    ContMDiffAt I 𝓘(𝕜, E) n (e.extend I) x :=
  (contMDiff_model _).comp x <| contMDiffAt_of_mem_maximalAtlas he hx

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

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

Разделы

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

Аффилиация

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