OAI/GroupTheory/SimpleAmenable/PolygonGeometry/CompactFineGrid.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.closedWindowBox line 14
  2. theorem OAI.SimpleAmenable.closedWindowBox_subset line 18
  3. theorem OAI.SimpleAmenable.closedWindowBox_nonempty line 28
  4. theorem OAI.SimpleAmenable.windowPlanarLift_zero line 40
  5. theorem OAI.SimpleAmenable.windowRectangle_subset_closed line 48
  6. theorem OAI.SimpleAmenable.compact_open_cover_fine_grid line 57
  7. theorem OAI.SimpleAmenable.compact_local_bounds_fine_grid line 84
  8. theorem OAI.SimpleAmenable.vertex_type_zero line 116
  9. theorem OAI.SimpleAmenable.ordinary_pair_near line 122
  10. theorem OAI.SimpleAmenable.ConcurrentGeometry.simultaneous_active_template line 133
  11. theorem OAI.SimpleAmenable.ConcurrentGeometry.simultaneous_active_neighborhood line 171