contMDiffAt_extChartAt — Mathlib

English

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

Русский

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

LaTeX

$$$\mathrm{ContMDiffAt}\; I\, 𝓘(\mathbb{C}, E)\ n\, (\mathrm{extChartAt}\ I\ x)\ x$$$

Lean4

theorem contMDiffAt_extChartAt : ContMDiffAt I 𝓘(𝕜, E) n (extChartAt I x) x :=
  by
  rw [contMDiffAt_iff_source]
  apply contMDiffWithinAt_id.congr_of_eventuallyEq_of_mem _ (by simp)
  filter_upwards [extChartAt_target_mem_nhdsWithin x] with y hy
  exact PartialEquiv.right_inv (extChartAt I x) hy

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