chore(topology/fiber_bundle): move trivializations to a new file (#17463

) Split the file `topology.fiber_bundle` into two, `topology.fiber_bundle.trivialization` and `topology.fiber_bundle.basic`, the former treating (pre)trivializations and the latter treating fiber bundles and constructions for them (the core construction, the prebundle construction, etc). Also move lemmas from `topology.vector_bundle.basic` which turned out not to invove the linear structure (cf [this discussion](#17359 (comment))) into `topology.fiber_bundle.trivialization`.
leanprover-community · Nov 10, 2022 · 0b00e53 · 0b00e53
1 parent 18b3881
commit 0b00e53
Show file tree

Hide file tree

Showing 5 changed files with 717 additions and 694 deletions.
diff --git a/src/analysis/complex/re_im_topology.lean b/src/analysis/complex/re_im_topology.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import analysis.complex.basic
-import topology.fiber_bundle
+import topology.fiber_bundle.basic
 
 /-!
 # Closure, interior, and frontier of preimages under `re` and `im`

diff --git a/src/topology/covering.lean b/src/topology/covering.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Thomas Browning
 -/
 import topology.is_locally_homeomorph
-import topology.fiber_bundle
+import topology.fiber_bundle.basic
 
 /-!
 # Covering Maps