OAI/GroupTheory/SimpleAmenable/PolygonGeometry/WindowCellPartition.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.finite_interval_cell line 15
  2. def OAI.SimpleAmenable.windowCell line 38
  3. def OAI.SimpleAmenable.liftedCoordinate line 41
  4. theorem OAI.SimpleAmenable.liftedCoordinate_bounds line 44
  5. theorem OAI.SimpleAmenable.windowCell_mem line 51
  6. theorem OAI.SimpleAmenable.windowCell_cover line 77
  7. theorem OAI.SimpleAmenable.windowCell_pairwise_disjoint line 87
  8. def OAI.SimpleAmenable.orientedPoint line 106
  9. theorem OAI.SimpleAmenable.orientedPoint_coordinate line 109
  10. theorem OAI.SimpleAmenable.orientedPoint_label line 113
  11. theorem OAI.SimpleAmenable.orientedPoint_tangent line 118
  12. structure OAI.SimpleAmenable.OldStripPair line 122
  13. def OAI.SimpleAmenable.OldStripPair.displacement line 145
  14. def OAI.SimpleAmenable.OldStripPair.firstCenter line 147
  15. theorem OAI.SimpleAmenable.OldStripPair.displacement_ordinary line 149
  16. theorem OAI.SimpleAmenable.OldStripPair.left_center_label line 152
  17. theorem OAI.SimpleAmenable.OldStripPair.right_base_label line 160
  18. theorem OAI.SimpleAmenable.int_natAbs_le_div_succ line 167
  19. theorem OAI.SimpleAmenable.InitialCoverSystem.separated_old_rectangles_commute line 179