Commit 2022-11-17 16:08 87f3aec4

chore(topology/{fiber,vector}_bundle/*): reorganize files (#17559) The PR #17505 was a big refactor but left declarations in place. This PR proposes a reorganization to clean up:

• new file topology.fiber_bundle.is_homeomorphic_trivial_bundle for the legacy is_homeomorphic_trivial_fiber_bundle construction (see discussion)
• new file topology.fiber_bundle.constructions covering the trivial, fibrewise-product and pullback fiber bundles. The trivial-bundle material was previously split between topology.{fiber,vector}_bundle.basic, the prod material was previously in topology.vector_bundle.prod, the pullback material was previously in topology.vector_bundle.pullback
• new file topology.vector_bundle.constructions covering the trivial, direct-sum and pullback vector bundles. The trivial-bundle material was previously in topology.vector_bundle.basic, the prod material was previously in topology.vector_bundle.prod, the pullback material was previously in topology.vector_bundle.pullback
• delete files topology.vector_bundle.prod and topology.vector_bundle.pullback, whose material has all been moved elsewhere
• delete construction trivialization.comap, which was morally (though not literally) a duplicate of trivialization.pullback
• cleaner proof of trivialization.prod.open_source, removing a spurious dependence on an ambient fiber bundle structure
• updated and augmented docs