mathlib

0b00e53a - chore(topology/fiber_bundle): move trivializations to a new file (#17463)

chore(topology/fiber_bundle): move trivializations to a new file (#17463) Split the file `topology.fiber_bundle` into two, `topology.fiber_bundle.trivialization` and `topology.fiber_bundle.basic`, the former treating (pre)trivializations and the latter treating fiber bundles and constructions for them (the core construction, the prebundle construction, etc). Also move lemmas from `topology.vector_bundle.basic` which turned out not to invove the linear structure (cf [this discussion](https://github.com/leanprover-community/mathlib/pull/17359#discussion_r1015622110)) into `topology.fiber_bundle.trivialization`.