mathlib3

74d3270e - fix(topology/topological_fiber_bundle): fix definition, review (#6184)

fix(topology/topological_fiber_bundle): fix definition, review (#6184) * fix definition of `is_topological_fiber_bundle`; * add `is_trivial_topological_fiber_bundle`; * more lemmas, golf here and there; * define induced fiber bundle.