mathlib

d9dcf699 - feat(topology/topological_fiber_bundle): a new standard construction for topological fiber bundles (#7935)

feat(topology/topological_fiber_bundle): a new standard construction for topological fiber bundles (#7935) In this PR we implement a new standard construction for topological fiber bundles: namely a structure that permits to define a fiber bundle when trivializations are given as local equivalences but there is not yet a topology on the total space. The total space is hence given a topology in such a way that there is a fiber bundle structure for which the local equivalences are also local homeomorphism and hence local trivializations.