contMDiffOn_extChartAt_symm — Mathlib

English

The symmetric extension is C^n on the image/range.

Русский

Симметричное продолжение гладно на изображении.

LaTeX

$$$\mathrm{ContMDiffOn}\; I\; I\, n\; (\mathrm{extChartAt}\ I x)^{\mathrm{symm}}\; \mathrm{range}\ I$$$

Lean4

theorem contMDiffOn_extChartAt_symm (x : M) : ContMDiffOn 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target :=
  by
  convert contMDiffOn_extend_symm (chart_mem_maximalAtlas (I := I) x)
  · rw [extChartAt_target, I.image_eq]
  · infer_instance
  · infer_instance

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