Mathlib Map

Theorems · Inductive type · convex and discrete geometry

Delone.DeloneSet

(X : Type u_3) → [MetricSpace X] → Type u_3

A Delone set consists of a set together with explicit radii witnessing uniform discreteness and relative denseness.

Defined in
Mathlib.Analysis.AperiodicOrder.Delone.Basic
Cited by
34 results in Mathlib
Foundations
Depth 1 from the axioms · uses no axioms
Assumes
MetricSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Delone.DeloneSet.packingRadius · cited by 16DeloneSet.packingRadiusDelone.DeloneSet.carrier · cited by 15DeloneSet.carrierDelone.DeloneSet.coveringRadius · cited by 14DeloneSet.coveringRadiusDelone.DeloneSet.mapIsometry · cited by 9DeloneSet.mapIsometryDelone.DeloneSet.mapBilipschitz · cited by 7DeloneSet.mapBilipschitzDelone.DeloneSet.ext · cited by 6DeloneSet.extDelone.DeloneSet.copy · cited by 3DeloneSet.copyDelone.DeloneSet.mk.congr_simp · cited by 2mk.congr_simpDelone.DeloneSet.isCover_coveringRadius · cited by 2DeloneSet.isCover_coverin…Delone.DeloneSet.toSet · cited by 2DeloneSet.toSetDelone.DeloneSet.mk.inj · cited by 1mk.injDelone.DeloneSet.mk.noConfusion · cited by 1mk.noConfusionDelone.DeloneSet.eq_of_mem_ball · cited by 1DeloneSet.eq_of_mem_ballDelone.DeloneSet.isSeparated_packingRadius · cited by 1DeloneSet.isSeparated_pac…Delone.DeloneSet.mapBilipschitz_carrier · cited by 1DeloneSet.mapBilipschitz_…MetricSpace · cited by 1684MetricSpaceDelone.DeloneSetCITED BYCITES

Cites1

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

Cited by47

Results whose statement or proof uses this declaration.