feat: port Topology.MetricSpace.Lipschitz (#2634)

leanprover-community · Mar 6, 2023 · aeba075 · aeba075
1 parent 342815a
commit aeba075
Show file tree

Hide file tree

Showing 2 changed files with 691 additions and 0 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1310,6 +1310,7 @@ import Mathlib.Topology.MetricSpace.EMetricParacompact
 import Mathlib.Topology.MetricSpace.EMetricSpace
 import Mathlib.Topology.MetricSpace.Equicontinuity
 import Mathlib.Topology.MetricSpace.Infsep
+import Mathlib.Topology.MetricSpace.Lipschitz
 import Mathlib.Topology.MetricSpace.MetricSeparated
 import Mathlib.Topology.MetricSpace.ShrinkingLemma
 import Mathlib.Topology.NhdsSet