contMDiffWithinAt_extChartAt_symm_range

English

Symmetric extension is smooth on the target.

Русский

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

LaTeX

$$$\mathrm{ContMDiffOn}\; (\mathrm{extChartAt}\ I x)^{\mathrm{symm}} \; (\mathrm{target})$$$

Lean4

theorem contMDiffWithinAt_extChartAt_symm_range (x : M) {y : E} (hy : y ∈ (extChartAt I x).target) :
    ContMDiffWithinAt 𝓘(𝕜, E) I n (extChartAt I x).symm (range I) y :=
  (contMDiffWithinAt_extChartAt_symm_target x hy).mono_of_mem_nhdsWithin (extChartAt_target_mem_nhdsWithin_of_mem hy)

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