OAI/Analysis/CircleDomains/Transfer/GraphGridCells.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Equal-scale three-dimensional cells, colored by sixteen residues in each coordinate. Enlarged balls in one color are disjoint.

  1. abbrev OAI.CircleDomainRigidity.GraphGridColor line 11
  2. abbrev OAI.CircleDomainRigidity.GraphGridIndex line 12
  3. abbrev OAI.CircleDomainRigidity.GraphSpace line 13
  4. def OAI.CircleDomainRigidity.graphGridInterval line 15
  5. def OAI.CircleDomainRigidity.graphGridCell line 18
  6. lemma OAI.CircleDomainRigidity.graphGridCell_dist_gt line 22
  7. lemma OAI.CircleDomainRigidity.graphGridCell_enlarged_disjoint line 44
  8. lemma OAI.CircleDomainRigidity.exists_graphGridInterval line 56
  9. lemma OAI.CircleDomainRigidity.exists_graphGridCell line 76
  10. lemma OAI.CircleDomainRigidity.graphGridCell_dist_le line 83