Skip to content

Commit 2acd194

Browse files
committed
feat: port Topology.VectorBundle.Basic (#4187)
1 parent 7634824 commit 2acd194

File tree

2 files changed

+1074
-0
lines changed

2 files changed

+1074
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2341,6 +2341,7 @@ import Mathlib.Topology.UniformSpace.UniformConvergenceTopology
23412341
import Mathlib.Topology.UniformSpace.UniformEmbedding
23422342
import Mathlib.Topology.UnitInterval
23432343
import Mathlib.Topology.UrysohnsLemma
2344+
import Mathlib.Topology.VectorBundle.Basic
23442345
import Mathlib.Util.AddRelatedDecl
23452346
import Mathlib.Util.AssertNoSorry
23462347
import Mathlib.Util.AtomM

0 commit comments

Comments
 (0)