contMDiffAt_extChartAt' — Mathlib

English

Extending a chart and taking the symmetric chart preserves C^n differentiability at a point.

Русский

Расширение чарта и симметризация сохраняют гладкость порядка n в точке.

LaTeX

$$$\mathrm{contMDiffAt\_extend}(...)$$$

Lean4

theorem contMDiffAt_extChartAt' {x' : M} (h : x' ∈ (chartAt H x).source) :
    ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x' :=
  contMDiffAt_extend (chart_mem_maximalAtlas x) h

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