OAI/Analysis/RieszRectifiability/Nets/ClosedNetCellCover.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Covering by closed net cells

The geometric decay of lattice radii lets fine net points approximate every point of the underlying set. Ancestor forcing places relative balls inside their closed cells, while properness reduces nearby ancestors to finitely many choices and yields a closed-cell cover.

  1. theorem OAI.RieszRectifiability.exists_latticeRadius_tail_lt line 20
  2. theorem OAI.RieszRectifiability.relative_ball_subset_closedNetCell line 28
  3. theorem OAI.RieszRectifiability.exists_closedNetCell_containing line 51