OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonAction.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.SimpleAmenable.(instance at line 12) line 12
  2. theorem OAI.SimpleAmenable.fract_fract_add line 14
  3. def OAI.SimpleAmenable.translate line 18
  4. theorem OAI.SimpleAmenable.translate_val line 30
  5. theorem OAI.SimpleAmenable.translate_zero line 34
  6. theorem OAI.SimpleAmenable.translate_add line 39
  7. def OAI.SimpleAmenable.translation line 46
  8. theorem OAI.SimpleAmenable.translation_apply line 52
  9. theorem OAI.SimpleAmenable.translation_mul line 55
  10. theorem OAI.SimpleAmenable.translation_period line 60
  11. theorem OAI.SimpleAmenable.translation_reduce line 66
  12. theorem OAI.SimpleAmenable.halfPlane_mem line 77
  13. def OAI.SimpleAmenable.wrapIndices line 81
  14. def OAI.SimpleAmenable.wrapCell line 85
  15. theorem OAI.SimpleAmenable.wrapCell_mem line 91
  16. theorem OAI.SimpleAmenable.mem_wrapCell line 97
  17. theorem OAI.SimpleAmenable.floor_wrap_mem line 109
  18. theorem OAI.SimpleAmenable.point_wrap_mem line 115
  19. theorem OAI.SimpleAmenable.translate_on_wrap line 120
  20. theorem OAI.SimpleAmenable.preimage_halfPlane line 128
  21. theorem OAI.SimpleAmenable.polygon_preimage_translate line 153
  22. theorem OAI.SimpleAmenable.polygon_image_translation line 165
  23. theorem OAI.SimpleAmenable.exists_in_interval_avoiding line 171
  24. theorem OAI.SimpleAmenable.generic_rectangle line 178
  25. instance OAI.SimpleAmenable.(instance at line 212) line 212