Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit f4fe790

Browse files
committed
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.
1 parent 60371b8 commit f4fe790

File tree

1 file changed

+203
-164
lines changed

1 file changed

+203
-164
lines changed

0 commit comments

Comments
 (0)