OAI/GroupTheory/SimpleAmenable/PolygonGeometry/WindowIntervals.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.coordinateShift_sub line 14
  2. theorem OAI.SimpleAmenable.coordinateBetween_reverse line 18
  3. theorem OAI.SimpleAmenable.coordinateBetween_empty line 30
  4. theorem OAI.SimpleAmenable.coordinate_window_between_resolved_all line 34
  5. theorem OAI.SimpleAmenable.coordinateBetween_period line 52
  6. theorem OAI.SimpleAmenable.coordinateLabelWindow_resolved line 72
  7. theorem OAI.SimpleAmenable.SameActionOn.mono line 99
  8. theorem OAI.SimpleAmenable.SameActionOn.comp line 102
  9. theorem OAI.SimpleAmenable.alphabetPerfect line 107
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.initialAlphabet_zero line 115
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_control_enlarged line 119
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.geometricSector_conditional_move line 137