OAI/Combinatorics/EditApproximation/Geometry/GroupCells.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Whole rational cells are enumerated by bounded ranges of grid indices.

  1. theorem OAI.EditApproximation.cellGridPoints_mem line 15
  2. theorem OAI.EditApproximation.cellGridPoints_length_le line 52
  3. theorem OAI.EditApproximation.cellTargetStates_mem line 68
  4. theorem OAI.EditApproximation.cellTargetStates_length_le line 94
  5. theorem OAI.EditApproximation.cellTargetStates_diameter line 104
  6. theorem OAI.EditApproximation.seedGridSpacing_covers_dyadic line 120
  7. def OAI.EditApproximation.targetCell line 131
  8. theorem OAI.EditApproximation.targetCell_contains line 134
  9. theorem OAI.EditApproximation.cellRepresentativeStates_mem_representatives line 147
  10. theorem OAI.EditApproximation.cellRepresentativeStates_length_le line 158
  11. theorem OAI.EditApproximation.cellRepresentativeStates_contains line 178