mathlib

8429ec96 - feat(topology/vector_bundle): `topological_vector_prebundle` (#8154)

feat(topology/vector_bundle): `topological_vector_prebundle` (#8154) In this PR we implement a new standard construction for topological vector bundles: namely a structure that permits to define a vector bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a vector bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.