contMDiff_tangentBundleModelSpaceHomeomorph

English

The map tangentBundleModelSpaceHomeomorph I: TangentBundle I H → ModelProd H E is C^n (continuously differentiable to order n) in the manifold sense.

Русский

Отображение tangentBundleModelSpaceHomeomorph I: TangentBundle I H → ModelProd H E гладко в смысле гладкости до порядка n.

LaTeX

$$$\text{ContMDiff I.tangent } (I.prod 𝓘(𝕜,E))\, n\; (tangentBundleModelSpaceHomeomorph I) :\; TangentBundle I H \to ModelProd H E,$$$

Lean4

theorem contMDiff_tangentBundleModelSpaceHomeomorph :
    ContMDiff I.tangent (I.prod 𝓘(𝕜, E)) n (tangentBundleModelSpaceHomeomorph I : TangentBundle I H → ModelProd H E) :=
  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
  simp [PartialEquiv.prod]

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