Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mk.inj

∀ {X : Type u_3} {inst : MetricSpace X} {carrier : Set X} {packingRadius : NNReal}
  {packingRadius_pos : 0 < packingRadius} {isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier}
  {coveringRadius : NNReal} {coveringRadius_pos : 0 < coveringRadius}
  {isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier} {carrier_1 : Set X}
  {packingRadius_1 : NNReal} {packingRadius_pos_1 : 0 < packingRadius_1}
  {isSeparated_packingRadius_1 : Metric.IsSeparated (↑packingRadius_1) carrier_1} {coveringRadius_1 : NNReal}
  {coveringRadius_pos_1 : 0 < coveringRadius_1}
  {isCover_coveringRadius_1 : Metric.IsCover coveringRadius_1 Set.univ carrier_1},
  { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
        isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
        coveringRadius_pos := coveringRadius_pos, isCover_coveringRadius := isCover_coveringRadius } =
      { carrier := carrier_1, packingRadius := packingRadius_1, packingRadius_pos := packingRadius_pos_1,
        isSeparated_packingRadius := isSeparated_packingRadius_1, coveringRadius := coveringRadius_1,
        coveringRadius_pos := coveringRadius_pos_1, isCover_coveringRadius := isCover_coveringRadius_1 } →
    carrier = carrier_1 ∧ packingRadius = packingRadius_1 ∧ coveringRadius = coveringRadius_1

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

1 results in Mathlib

Foundations

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