OAI/GroupTheory/SimpleAmenable/PolygonGeometry/Supported.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.SupportedIn line 12
  2. theorem OAI.SimpleAmenable.supported_disjoint_commute line 15
  3. theorem OAI.SimpleAmenable.supported_conjugate line 24
  4. theorem OAI.SimpleAmenable.double_commutator_of_displacement line 35
  5. theorem OAI.SimpleAmenable.supported_double_commutator line 47
  6. theorem OAI.SimpleAmenable.ordinary_denseRange line 54
  7. theorem OAI.SimpleAmenable.exists_cut_between line 67
  8. instance OAI.SimpleAmenable.(instance at line 71) line 71
  9. instance OAI.SimpleAmenable.(instance at line 74) line 74
  10. theorem OAI.SimpleAmenable.cutForm_continuous line 77
  11. theorem OAI.SimpleAmenable.halfPlane_isClopen line 84
  12. theorem OAI.SimpleAmenable.polygon_isClopen line 95
  13. theorem OAI.SimpleAmenable.generic_coordinates_pos line 99
  14. theorem OAI.SimpleAmenable.polygon_contains_rectangle line 105
  15. def OAI.SimpleAmenable.smallSquare line 137
  16. theorem OAI.SimpleAmenable.mem_smallSquare line 141
  17. theorem OAI.SimpleAmenable.smallSquare_nonempty line 144
  18. def OAI.SimpleAmenable.fiveRectangleShifts line 151
  19. theorem OAI.SimpleAmenable.fiveRectangleShifts_val line 154
  20. theorem OAI.SimpleAmenable.five_slots_in_polygon line 172
  21. def OAI.SimpleAmenable.translatedPolygon line 231
  22. theorem OAI.SimpleAmenable.floor_remainder_bounds line 235
  23. theorem OAI.SimpleAmenable.smallSquare_finite_translated_cover line 254
  24. def OAI.SimpleAmenable.bankIndex line 286
  25. def OAI.SimpleAmenable.bankPermutation line 288
  26. theorem OAI.SimpleAmenable.bankPermutation_even line 291
  27. theorem OAI.SimpleAmenable.bankPermutation_apply line 295
  28. def OAI.SimpleAmenable.bankSlots line 299
  29. theorem OAI.SimpleAmenable.bankSlots_apply line 303
  30. theorem OAI.SimpleAmenable.bankSlots_injective line 308
  31. theorem OAI.SimpleAmenable.transport_bank line 329
  32. theorem OAI.SimpleAmenable.slot_ranges_disjoint_of_tracks line 346
  33. theorem OAI.SimpleAmenable.slots_injective_of_tracks line 355
  34. theorem OAI.SimpleAmenable.fresh_nine_tracks line 366
  35. theorem OAI.SimpleAmenable.transport_three_slots line 389