OAI/Analysis/CircleDomains/Probability/HausdorffZeroCounting.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Zero-dimensional Hausdorff measure counts the points of an arbitrary set. Finite subsets suffice for the lower bound on infinite sets.

  1. lemma OAI.CircleDomainRigidity.hausdorff_zero_finset line 13
  2. lemma OAI.CircleDomainRigidity.hausdorff_zero_eq_count line 19