feat: port Topology.Category.Top.Opens (#3662)

leanprover-community · Apr 27, 2023 · 48a2b71 · 48a2b71
1 parent 850e670
commit 48a2b71
Show file tree

Hide file tree

Showing 2 changed files with 420 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1902,6 +1902,7 @@ import Mathlib.Topology.Category.Born
 import Mathlib.Topology.Category.Top.Adjunctions
 import Mathlib.Topology.Category.Top.Basic
 import Mathlib.Topology.Category.Top.EpiMono
+import Mathlib.Topology.Category.Top.Opens
 import Mathlib.Topology.CompactOpen
 import Mathlib.Topology.Connected
 import Mathlib.Topology.Constructions