Theorems · Definition · convex and discrete geometry

Delone.DeloneSet.casesOn

{X : Type u_3} →
  [inst : MetricSpace X] →
    {motive : Delone.DeloneSet X → Sort u} →
      (t : Delone.DeloneSet 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) →
                        motive
                          { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
                            isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
                            coveringRadius_pos := coveringRadius_pos,
                            isCover_coveringRadius := isCover_coveringRadius }) →
          motive t

Defined in

Mathlib.Analysis.AperiodicOrder.Delone.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

MetricSpace