Theorems · Definition · convex and discrete geometry

Delone.DeloneSet.mapIsometry

{X : Type u_1} →
  {Y : Type u_2} → [inst : MetricSpace X] → [inst_1 : MetricSpace Y] → X ≃ᵢ Y → Delone.DeloneSet X ≃ Delone.DeloneSet Y

The image of a Delone set under an isometry. This is a specialization of DeloneSet.mapBilipschitz where the packing and covering radii are preserved because the Lipschitz constants are both 1.

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

9 results in Mathlib

Foundations

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

Assumes

MetricSpaceMetricSpace