Skip to content

Commit b463603

Browse files
committed
chore(Lipschitz): split (#8264)
Move parts that don't need `MetricSpace`s to a new file.
1 parent aff5c83 commit b463603

File tree

3 files changed

+511
-465
lines changed

3 files changed

+511
-465
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3443,6 +3443,7 @@ import Mathlib.Topology.DenseEmbedding
34433443
import Mathlib.Topology.DiscreteQuotient
34443444
import Mathlib.Topology.DiscreteSubset
34453445
import Mathlib.Topology.EMetricSpace.Basic
3446+
import Mathlib.Topology.EMetricSpace.Lipschitz
34463447
import Mathlib.Topology.EMetricSpace.Paracompact
34473448
import Mathlib.Topology.ExtendFrom
34483449
import Mathlib.Topology.ExtremallyDisconnected

0 commit comments

Comments
 (0)