OAI/MeasureTheory/Falconer/Geometry/OccupiedCellSeparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separation extends from the full source set to sufficiently small occupied cells

  1. theorem OAI.Falconer.exists_mem_cell_source line 12
  2. theorem OAI.Falconer.occupied_cell_separation line 20
  3. theorem OAI.Falconer.occupied_cell_center_separation line 34