contMDiff_tangentBundleModelSpaceHomeomorph_symm

English

The inverse of the tangent bundle model-space homeomorphism is ContMDiff.

Русский

Обратное отображение гомеоморфизма гомогенного пространства касательного пространства гладко дифференцируемо.

LaTeX

$$$\text{ContMDiff } (I.prod 𝓘(𝕜, E)) I.tangent n\ ((tangentBundleModelSpaceHomeomorph I).symm)$$$

Lean4

theorem contMDiff_tangentBundleModelSpaceHomeomorph_symm :
    ContMDiff (I.prod 𝓘(𝕜, E)) I.tangent n
      ((tangentBundleModelSpaceHomeomorph I).symm : ModelProd H E → TangentBundle I H) :=
  by
  apply contMDiff_iff.2 ⟨Homeomorph.continuous _, fun x y ↦ ?_⟩
  apply contDiffOn_id.congr
  simp only [mfld_simps, mem_range, TotalSpace.toProd, Equiv.coe_fn_symm_mk, forall_exists_index, Prod.forall,
    Prod.mk.injEq]
  rintro a b x rfl
  simpa [PartialEquiv.prod] using ⟨rfl, rfl⟩

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