mathlib

cf6f27ee - refactor(topology/{fiber_bundle, vector_bundle}): make trivializations data rather than an existential (#13052)

refactor(topology/{fiber_bundle, vector_bundle}): make trivializations data rather than an existential (#13052) Previously, the construction `topological_vector_bundle` was a mixin requiring the _existence_ of a suitable trivialization at each point. Change this to a class with data: a choice of trivialization at each point. This has no effect on the mathematics, but it is necessary for the forthcoming refactor in which a further condition is imposed on the mutual compatibility of the trivializations. Furthermore, attach to `topological_vector_bundle` and to two other constructions `topological_fiber_prebundle`, `topological_vector_prebundle` a further piece of data: an atlas of "good" trivializations. This is not really mathematically necessary, since you could always take the atlas of "good" trivializations to be simply the set of canonical trivializations at each point in the manifold. But sometimes one naturally has this larger "good" class and it's convenient to be able to access it. The `charted_space` definition in the manifolds library does something similar.