OAI/GroupTheory/SimpleAmenable/PolygonGeometry/InactiveNeighborhoodActions.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.strict_rectangle_ball line 14
  2. theorem OAI.SimpleAmenable.InitialCoverSystem.RectangularAtlas.inactive_near_action_neighborhood line 35
  3. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChartNeighborhood line 87
  4. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChartAnchor line 93
  5. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChartBound line 98
  6. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChartBoundaryAnchor line 105
  7. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChartBoundaryBound line 110
  8. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChart line 117
  9. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.vertex line 125
  10. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.offset line 126
  11. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.neighborhood line 127
  12. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.active_anchor line 128
  13. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.active_bound line 129
  14. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.boundary_anchor line 130
  15. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.boundary_bound line 131
  16. theorem OAI.SimpleAmenable.ConcurrentGeometry.inwardChart_exists line 134
  17. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.canonical_mem line 162
  18. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.assignment_realized line 168
  19. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.local_decisions_eq line 178
  20. def OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.polygons line 196
  21. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.polygons_assignment_realized line 200
  22. theorem OAI.SimpleAmenable.ConcurrentGeometry.InwardChart.polygons_locally_eq line 217