feat: port Topology.Sets.Opens (#2118)

Co-authored-by: Johan Commelin <johan@commelin.net>
leanprover-community · Feb 11, 2023 · f7cd1dc · f7cd1dc
1 parent 2e9fc2c
commit f7cd1dc
Show file tree

Hide file tree

Showing 2 changed files with 501 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1058,6 +1058,7 @@ import Mathlib.Topology.Order.Priestley
 import Mathlib.Topology.Paracompact
 import Mathlib.Topology.Perfect
 import Mathlib.Topology.Separation
+import Mathlib.Topology.Sets.Opens
 import Mathlib.Topology.ShrinkingLemma
 import Mathlib.Topology.Sober
 import Mathlib.Topology.StoneCech