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