mathlib

f12575e8 - feat(topology/topological_fiber_bundle): topological fiber bundle over `[a, b]` is trivial (#6555)