contMDiffOn_extend_symm — Mathlib

English

The symmetric extension of extChartAt is C^n-smooth on the target.

Русский

Симметричное продолжение extChartAt гладко по порядку n на целевой области.

LaTeX

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

Lean4

theorem contMDiffOn_extend_symm (he : e ∈ maximalAtlas I n M) :
    ContMDiffOn 𝓘(𝕜, E) I n (e.extend I).symm (I '' e.target) :=
  by
  refine (contMDiffOn_symm_of_mem_maximalAtlas he).comp (contMDiffOn_model_symm.mono <| image_subset_range _ _) ?_
  simp_rw [image_subset_iff, PartialEquiv.restr_coe_symm, I.toPartialEquiv_coe_symm, preimage_preimage, I.left_inv,
    preimage_id'];
  rfl

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