feat: port Topology.UniformSpace.AbstractCompletion (#2238)

leanprover-community · Feb 12, 2023 · 54e0758 · 54e0758
1 parent 15185f3
commit 54e0758
Show file tree

Hide file tree

Showing 2 changed files with 393 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1098,6 +1098,7 @@ import Mathlib.Topology.StoneCech
 import Mathlib.Topology.SubsetProperties
 import Mathlib.Topology.Support
 import Mathlib.Topology.UniformSpace.AbsoluteValue
+import Mathlib.Topology.UniformSpace.AbstractCompletion
 import Mathlib.Topology.UniformSpace.Basic
 import Mathlib.Topology.UniformSpace.Cauchy
 import Mathlib.Topology.UniformSpace.CompleteSeparated