feat(topology/vector_bundle): redefine continuous coordinate change (#14462)
feat(topology/vector_bundle): redefine continuous coordinate change (#14462)

* For any two trivializations, we define the coordinate change between the two trivializations: continous linear automorphism of `F`, defined by composing one trivialization with the inverse of the other. This is defined for any point in the intersection of their base sets, and we define it to be the identity function outside this set.
* Redefine `topological_vector_bundle`: we now require that this coordinate change between any two trivializations is continuous on the intersection of their base sets.
* Redefine `topological_vector_prebundle` with the existence of a continuous linear coordinate change function.
* Simplify the proofs that the coordinate change function is continuous for constructions on vector bundles.





leanprover-community/mathlib,leanprover-community/mathlib