OAI/Analysis/CircleDomains/Topology/EqualScaleCellSeparation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed finite coloring separates the enlarged equal-scale cells. This supplies bounded overlap without assuming measure doubling.

  1. lemma OAI.CircleDomainRigidity.equal_scale_cell_separation line 11