Fiber bundle Construction Theorem

Stream: Is there code for X?

[Dominic Steinitz]

In my steps to constructing a principal fiber bundle, I have managed to construct the Mobius band as both a fiber bundle and a vector bundle without seeming to ever specify the total space (one only needs to specify coordinate transformation functions). But now to show that the Mobius band is actually smooth I think I need to show my vector bundle is an instance of ContMDiffVectorBundle and now I think I really do need the local trivialisations. Here's the definition for reference

variable [TopologicalSpace (TotalSpace F E)] [∀ x, TopologicalSpace (E x)] (F E)
variable [FiberBundle F E] [VectorBundle 𝕜 F E]

variable (n IB) in
/-- When `B` is a manifold with respect to a model `IB` and `E` is a
topological vector bundle over `B` with fibers isomorphic to `F`,
then `ContMDiffVectorBundle n F E IB` registers that the bundle is `C^n`, in the sense of having
`C^n` transition functions. This is a mixin, not carrying any new data. -/
class ContMDiffVectorBundle : Prop where
  protected contMDiffOn_coordChangeL :
    ∀ (e e' : Trivialization F (π F E)) [MemTrivializationAtlas e] [MemTrivializationAtlas e'],
      ContMDiffOn IB 𝓘(𝕜, F →L[𝕜] F) n (fun b : B => (e.coordChangeL 𝕜 e' b : F →L[𝕜] F))
        (e.baseSet ∩ e'.baseSet)

I don't think a theorem showing the existence of the total space as a manifold with local trivialisations from coordinate change maps exists but I would be happy to be wrong. If it does not exist then I will attempt to come up with one and any tips and advice would be very welcome.