# Commit 2021-02-12 12:44 74d3270e

View on Github →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.