feat: port Topology.UniformSpace.CompactConvergence (#2281)

leanprover-community · Feb 14, 2023 · 0f5ac2f · 0f5ac2f
1 parent f69c5e4
commit 0f5ac2f
Show file tree

Hide file tree

Showing 2 changed files with 455 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1128,6 +1128,7 @@ import Mathlib.Topology.UniformSpace.AbsoluteValue
 import Mathlib.Topology.UniformSpace.AbstractCompletion
 import Mathlib.Topology.UniformSpace.Basic
 import Mathlib.Topology.UniformSpace.Cauchy
+import Mathlib.Topology.UniformSpace.CompactConvergence
 import Mathlib.Topology.UniformSpace.CompleteSeparated
 import Mathlib.Topology.UniformSpace.Equiv
 import Mathlib.Topology.UniformSpace.Pi