mathlib

a30375e0 - feat(topology/fiber_bundle): a topological fiber bundle is a quotient map (#11194)

feat(topology/fiber_bundle): a topological fiber bundle is a quotient map (#11194) * The projection map of a topological fiber bundle (pre)trivialization is surjective onto its base set. * The projection map of a topological fiber bundle with a nonempty fiber is surjective. Since it is also a continuous open map, it is a quotient map. * Golf a few proofs.