contMDiff_snd_tangentBundle_modelSpace

English

The second projection on tangentBundleModelSpace model space is C^n after composing with tangentBundleModelSpaceHomeomorph.

Русский

Вторая проекция после композиции с tangentBundleModelSpaceHomeomorph гладкая до порядка n.

LaTeX

$$$\text{ContMDiff}_{n} \bigl( (tangentBundleModelSpaceHomeomorph I) : TangentBundle I H \to ModelProd H E \bigr) \circ \mathrm{Prod}_2$$$

Lean4

/-- In the tangent bundle to the model space, the second projection is `C^n`. -/
theorem contMDiff_snd_tangentBundle_modelSpace : ContMDiff I.tangent 𝓘(𝕜, E) n (fun (p : TangentBundle I H) ↦ p.2) :=
  by
  change ContMDiff I.tangent 𝓘(𝕜, E) n ((id Prod.snd : ModelProd H E → E) ∘ (tangentBundleModelSpaceHomeomorph I))
  apply ContMDiff.comp (I' := I.prod 𝓘(𝕜, E))
  · convert contMDiff_snd
    rw [chartedSpaceSelf_prod]
    rfl
  · exact contMDiff_tangentBundleModelSpaceHomeomorph

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