English
If a vector bundle E over B is C^n and modeled on F, then the total space of the bundle inherits a natural C^n-manifold structure.
Русский
Общее пространство окрашено как C^n-манифолд.
LaTeX
$$$$\\text{IsManifold }(\\text{TotalSpace }F E)\,,$$$$
Lean4
/-- A `C^n` vector bundle `E` is naturally a `C^n` manifold. -/
instance isManifold : IsManifold (IB.prod 𝓘(𝕜, F)) n (TotalSpace F E) :=
by
refine { StructureGroupoid.HasGroupoid.comp (contMDiffFiberwiseLinear B F IB n) ?_ with }
intro e he
rw [mem_contMDiffFiberwiseLinear_iff] at he
obtain ⟨φ, U, hU, hφ, h2φ, heφ⟩ := he
rw [isLocalStructomorphOn_contDiffGroupoid_iff]
refine ⟨ContMDiffOn.congr ?_ (EqOnSource.eqOn heφ), ContMDiffOn.congr ?_ (EqOnSource.eqOn (EqOnSource.symm' heφ))⟩
· rw [EqOnSource.source_eq heφ]
apply contMDiffOn_fst.prodMk
exact (hφ.comp contMDiffOn_fst <| prod_subset_preimage_fst _ _).clm_apply contMDiffOn_snd
· rw [EqOnSource.target_eq heφ]
apply contMDiffOn_fst.prodMk
exact (h2φ.comp contMDiffOn_fst <| prod_subset_preimage_fst _ _).clm_apply contMDiffOn_snd
