feat: port Topology.LocalExtr (#1909)

leanprover-community · Jan 31, 2023 · 1c27d1e · 1c27d1e
1 parent 195bf2a
commit 1c27d1e
Show file tree

Hide file tree

Showing 2 changed files with 635 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -926,6 +926,7 @@ import Mathlib.Topology.Bornology.Constructions
 import Mathlib.Topology.Bornology.Hom
 import Mathlib.Topology.Constructions
 import Mathlib.Topology.ContinuousOn
+import Mathlib.Topology.LocalExtr
 import Mathlib.Topology.LocallyFinite
 import Mathlib.Topology.Maps
 import Mathlib.Topology.NhdsSet