OAI/Combinatorics/EditApproximation/Geometry/ActualRoundedGroupInputs.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Every actual unskipped rounded group input belongs to a common small endpoint list determined by the cell, child and envelope label.

  1. theorem OAI.EditApproximation.groupRoundSpacing_pos line 14
  2. theorem OAI.EditApproximation.groupRoundSpacing_envelope_bound line 18
  3. theorem OAI.EditApproximation.bandRoundSpacing_group_spacing line 27
  4. theorem OAI.EditApproximation.gridStateBox_sound line 36
  5. theorem OAI.EditApproximation.actual_rounded_group_input_mem line 54
  6. theorem OAI.EditApproximation.groupRoundedStateList_length line 90