Commit 2022-01-04 13:36 a30375e0
View on Github →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.