OAI/GroupTheory/SimpleAmenable/PolygonGeometry/ConcurrentGeometry.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.ConcurrentGeometryData line 16
  2. abbrev OAI.SimpleAmenable.ConcurrentGeometry line 42
  3. theorem OAI.SimpleAmenable.concurrentGeometry_exists line 45
  4. theorem OAI.SimpleAmenable.ConcurrentGeometry.mesh_small line 86
  5. theorem OAI.SimpleAmenable.ConcurrentGeometry.margin_resolved line 91
  6. def OAI.SimpleAmenable.initialPatchPrimitives line 102
  7. structure OAI.SimpleAmenable.InitialCoverSystem.PatchAtlas line 111
  8. theorem OAI.SimpleAmenable.patchAtlas_eventually line 123
  9. theorem OAI.SimpleAmenable.closedWindow_diameter line 143
  10. theorem OAI.SimpleAmenable.windowRectangle_closed_intersection_near line 159
  11. theorem OAI.SimpleAmenable.ConcurrentGeometry.crossing_cell_template line 209