contMDiffWithinAt_extChartAt_symm_target_self

English

At the point extChartAt I x x, the symmetric extension is ContMDiffWithinAt of order n.

Русский

В точке extChartAt I x x симметричное продолжение является ContMDiffWithinAt порядка n.

LaTeX

$$$\mathrm{ContMDiffWithinAt}\, 𝓘(\mathbb{C}, E) I n (\mathrm{extChartAt}\ I x)^{\mathrm{symm}}.toFun (\mathrm{extChartAt}\ I x).target (\mathrm{extChartAt}\ I x x)$$$

Lean4

theorem contMDiffWithinAt_extChartAt_symm_target_self (x : M) :
    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (extChartAt I x).target (extChartAt I x x) :=
  by
  rw [contMDiffWithinAt_iff_target]
  constructor
  · apply ContinuousAt.continuousWithinAt
    apply ContinuousAt.comp _ I.continuousAt_symm
    exact (chartAt H x).symm.continuousAt (by simp)
  · apply contMDiffWithinAt_id.congr_of_mem (fun y hy ↦ ?_) (by simp)
    convert PartialEquiv.right_inv (extChartAt I x) hy
    simp

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