OAI/GroupTheory/SimpleAmenable/Amenability/BarrierCells.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.arrangementAtom line 16
  2. theorem OAI.SimpleAmenable.mem_arrangementAtom line 21
  3. def OAI.SimpleAmenable.arrangementPattern line 34
  4. theorem OAI.SimpleAmenable.mem_arrangementPattern line 38
  5. theorem OAI.SimpleAmenable.strictLineCell_convex line 48
  6. def OAI.SimpleAmenable.squareInterior line 60
  7. theorem OAI.SimpleAmenable.generic_mem_squareInterior line 62
  8. def OAI.SimpleAmenable.barrierRegion line 66
  9. def OAI.SimpleAmenable.SupportedBarriers line 68
  10. theorem OAI.SimpleAmenable.generic_mem_barrierRegion line 72
  11. theorem OAI.SimpleAmenable.arrangementAtom_same_component line 80
  12. def OAI.SimpleAmenable.barrierComponentCell line 101
  13. theorem OAI.SimpleAmenable.barrierComponentCell_polygon line 104
  14. structure OAI.SimpleAmenable.FinitePolygonPartition line 140
  15. def OAI.SimpleAmenable.barrierPolygonAt line 145
  16. theorem OAI.SimpleAmenable.barrierPolygonAt_eq_of_pattern line 150
  17. theorem OAI.SimpleAmenable.barrierPolygonAt_finite_range line 164
  18. def OAI.SimpleAmenable.finiteBarrierPartition line 177
  19. theorem OAI.SimpleAmenable.mem_finiteBarrierPartition line 197