Theorems · Theorem · convex and discrete geometry

Delone.DeloneSet.mk.congr_simp

∀ {X : Type u_3} [inst : MetricSpace X] (carrier carrier_1 : Set X) (e_carrier : carrier = carrier_1)
  (packingRadius packingRadius_1 : NNReal) (e_packingRadius : packingRadius = packingRadius_1)
  (packingRadius_pos : 0 < packingRadius) (isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier)
  (coveringRadius coveringRadius_1 : NNReal) (e_coveringRadius : coveringRadius = coveringRadius_1)
  (coveringRadius_pos : 0 < coveringRadius) (isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier),
  { 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 := ⋯, isSeparated_packingRadius := ⋯,
      coveringRadius := coveringRadius_1, coveringRadius_pos := ⋯, isCover_coveringRadius := ⋯ }

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

MetricSpace