Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mk.injEq

∀ {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

0 results in Mathlib

Foundations

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

Assumes

MetricSpace