feat: port Topology.Bases (#1910)

leanprover-community · Feb 1, 2023 · 3e45c8e · 3e45c8e
1 parent cdca999
commit 3e45c8e
Show file tree

Hide file tree

Showing 2 changed files with 897 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -921,6 +921,7 @@ import Mathlib.Testing.SlimCheck.Gen
 import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Topology.Algebra.Order.LeftRight
+import Mathlib.Topology.Bases
 import Mathlib.Topology.Basic
 import Mathlib.Topology.Bornology.Basic
 import Mathlib.Topology.Bornology.Constructions