OAI/GroupTheory/SimpleAmenable/PolygonGeometry/WindowRectangles.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.windowRectangle line 15
  2. def OAI.SimpleAmenable.windowPlanarLift line 20
  3. theorem OAI.SimpleAmenable.windowPlanarLift_coordinate line 24
  4. theorem OAI.SimpleAmenable.windowPlanarLift_spec line 28
  5. theorem OAI.SimpleAmenable.windowRectangle_mem line 35
  6. theorem OAI.SimpleAmenable.windowRectangle_cover line 45
  7. theorem OAI.SimpleAmenable.windowRectangle_pairwise_disjoint line 51
  8. theorem OAI.SimpleAmenable.windowRectangle_resolved line 64
  9. theorem OAI.SimpleAmenable.windowRectangle_diameter line 75
  10. theorem OAI.SimpleAmenable.linear_form_dist_bound line 93
  11. theorem OAI.SimpleAmenable.crossing_level_bound line 110
  12. theorem OAI.SimpleAmenable.line_point_in_box line 123
  13. theorem OAI.SimpleAmenable.windowRectangle_intersection_near line 145