Theorems · Definition · convex and discrete geometry

Delone.DeloneSet.mk.noConfusion

{X : Type u_3} →
  {inst : MetricSpace X} →
    {P : Sort u} →
      {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' : 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 := carrier, packingRadius := packingRadius,
                                        packingRadius_pos := packingRadius_pos,
                                        isSeparated_packingRadius := isSeparated_packingRadius,
                                        coveringRadius := coveringRadius, coveringRadius_pos := coveringRadius_pos,
                                        isCover_coveringRadius := isCover_coveringRadius } =
                                      { carrier := carrier', packingRadius := packingRadius',
                                        packingRadius_pos := packingRadius_pos',
                                        isSeparated_packingRadius := isSeparated_packingRadius',
                                        coveringRadius := coveringRadius', coveringRadius_pos := coveringRadius_pos',
                                        isCover_coveringRadius := isCover_coveringRadius' } →
                                    (carrier ≍ carrier' →
                                        packingRadius = packingRadius' → coveringRadius = coveringRadius' → P) →
                                      P

Defined in: Mathlib.Analysis.AperiodicOrder.Delone.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 157 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
NNRealstatement and proof · cited by 4,310
Set.univstatement and proof · cited by 3,945
MetricSpacestatement and proof · cited by 1,684
ENNReal.ofNNRealstatement and proof · cited by 1,279
Metric.IsCoverstatement and proof · cited by 51
Delone.DeloneSetstatement · cited by 34
Metric.IsSeparatedstatement and proof · cited by 28
Delone.DeloneSet.noConfusionproof · cited by 0

Cited by1

Results whose statement or proof uses this declaration.

Delone.DeloneSet.mk.injproof · cited by 1