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