OAI/Geometry/CylinderCovering/Nilpotent/Grid.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.NilpotentGrid.gridBound_nonneg line 9
  2. lemma OAI.NilpotentGrid.indexRange_card line 12
  3. lemma OAI.NilpotentGrid.candidates_card line 21
  4. lemma OAI.NilpotentGrid.mem_indexRange_of_cell line 27
  5. lemma OAI.NilpotentGrid.mem_coarseIndices_iff line 46
  6. lemma OAI.NilpotentGrid.floor_cell line 57
  7. lemma OAI.NilpotentGrid.subset_coarseUnion line 67
  8. theorem OAI.NilpotentGrid.coarse_count_bound line 78
  9. lemma OAI.NilpotentGrid.same_cell_distance line 99
  10. theorem OAI.NilpotentGrid.coarseUnion_near line 121
  11. lemma OAI.NilpotentGrid.coarseCell_isCompact line 131
  12. lemma OAI.NilpotentGrid.coarseUnion_isCompact line 148