Skip to content

Commit 8885835

Browse files
committed
feat: define Metric.Snowflaking (#33114)
From https://github.com/urkud/SardMoreira This is a copy of the original space with distance redefined to be `d x y = (dist x y) ^ α`.
1 parent 05f342b commit 8885835

File tree

3 files changed

+521
-0
lines changed

3 files changed

+521
-0
lines changed

Mathlib.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7240,6 +7240,7 @@ public import Mathlib.Topology.MetricSpace.Pseudo.Real
72407240
public import Mathlib.Topology.MetricSpace.Sequences
72417241
public import Mathlib.Topology.MetricSpace.ShrinkingLemma
72427242
public import Mathlib.Topology.MetricSpace.Similarity
7243+
public import Mathlib.Topology.MetricSpace.Snowflaking
72437244
public import Mathlib.Topology.MetricSpace.ThickenedIndicator
72447245
public import Mathlib.Topology.MetricSpace.Thickening
72457246
public import Mathlib.Topology.MetricSpace.TransferInstance

0 commit comments

Comments
 (0)