Commit 2022-06-01 12:13 f4fe7907

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.