refactor(topology/vector_bundle): split file (#14535)

Also: * Rename `pullback` -> `topological_vector_bundle.pullback` * Use `delta_instance` instead of `local attribute [reducible]` * Change module doc * Remove transitive import
leanprover-community · Jun 4, 2022 · 93fb534 · 93fb534
1 parent 3103a89
commit 93fb534
Show file tree

Hide file tree

Showing 4 changed files with 392 additions and 375 deletions.
diff --git a/src/geometry/manifold/tangent_bundle.lean b/src/geometry/manifold/tangent_bundle.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
-import topology.vector_bundle
+import topology.vector_bundle.basic
 import geometry.manifold.smooth_manifold_with_corners
 import data.set.prod