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.





leanprover-community/mathlib,leanprover-community/mathlib