OAI/Geometry/PeriodicTiling/ResidueTransversal.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.residueSuccessor line 17
  2. theorem OAI.PeriodicTilingThree.exists_residue_pairs line 23
  3. def OAI.PeriodicTilingThree.residuePairs line 32
  4. theorem OAI.PeriodicTilingThree.residuePairs_step line 37
  5. theorem OAI.PeriodicTilingThree.residuePairs_ne_zero line 43
  6. def OAI.PeriodicTilingThree.residuePairGood line 48
  7. theorem OAI.PeriodicTilingThree.normalized_bad_assignment_ratio line 53
  8. theorem OAI.PeriodicTilingThree.residuePairGood_card line 70
  9. theorem OAI.PeriodicTilingThree.representative_difference_of_pairGood line 78
  10. theorem OAI.PeriodicTilingThree.exists_good_pair line 86
  11. theorem OAI.PeriodicTilingThree.exists_simultaneous_good_pairs line 96
  12. theorem OAI.PeriodicTilingThree.exists_rigid_assignment_of_requests line 122
  13. theorem OAI.PeriodicTilingThree.exists_rigid_assignment64 line 158
  14. def OAI.PeriodicTilingThree.rigidAssignment64 line 165
  15. theorem OAI.PeriodicTilingThree.rigidAssignment64_difference line 168
  16. def OAI.PeriodicTilingThree.rigidSection line 173
  17. theorem OAI.PeriodicTilingThree.rigidSection_difference line 177
  18. theorem OAI.PeriodicTilingThree.section_difference_to_Tstar line 181
  19. theorem OAI.PeriodicTilingThree.rigidSection_Tstar_difference line 193