Theorems · Definition · convex and discrete geometry

Delone.DeloneSet.copy

{X : Type u_1} →
  [inst : MetricSpace X] →
    (D : Delone.DeloneSet X) →
      (carrier : Set X) →
        (packingRadius coveringRadius : NNReal) →
          carrier = D.carrier → packingRadius = D.packingRadius → coveringRadius = D.coveringRadius → Delone.DeloneSet X

Copy of a Delone set with new fields equal to the old ones. Useful to fix definitional equalities.

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

MetricSpace