Theorems · Definition · convex and discrete geometry

Delone.DeloneSet.mapBilipschitz

{X : Type u_1} →
  {Y : Type u_2} →
    [inst : MetricSpace X] →
      [inst_1 : MetricSpace Y] →
        (f : X ≃ Y) →
          (K₁ K₂ : NNReal) →
            0 < K₁ → 0 < K₂ → AntilipschitzWith K₁ ⇑f → LipschitzWith K₂ ⇑f → Delone.DeloneSet X → Delone.DeloneSet Y

Bilipschitz maps send Delone sets to Delone sets.

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

7 results in Mathlib

Foundations

Depth 154 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

MetricSpaceMetricSpace