mathlib

525c5a81 - feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber (#16079)

feat(topology/fiber_bundle): Each fiber of a trivialization is homeomorphic to the specified fiber (#16079) This PR adds `topological_fiber_bundle.trivialization.preimage_singleton_homeomorph`, which states that each fiber of a trivialization is homeomorphic to the specified fiber.