OAI/GroupTheory/SimpleAmenable/PolygonGeometry/SortedAxisCuts.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.sortedAxisCutSequence line 15
  2. def OAI.SimpleAmenable.labelLift line 69
  3. theorem OAI.SimpleAmenable.endpointLabel_labelLift line 72
  4. theorem OAI.SimpleAmenable.labelLift_bounds line 75
  5. theorem OAI.SimpleAmenable.labelLift_eq line 82
  6. def OAI.SimpleAmenable.anchorCutSet line 90
  7. theorem OAI.SimpleAmenable.anchorCutSet_lower line 95
  8. theorem OAI.SimpleAmenable.anchorCutSet_upper line 99
  9. theorem OAI.SimpleAmenable.anchorCutSet_bounds line 103
  10. theorem OAI.SimpleAmenable.anchorCutSet_labels line 113
  11. theorem OAI.SimpleAmenable.mem_anchorCutSet line 125
  12. theorem OAI.SimpleAmenable.sortedAxisCutSequence_mem line 154
  13. theorem OAI.SimpleAmenable.sortedAxisCutSequence_range line 157
  14. theorem OAI.SimpleAmenable.sortedAxisCutSequence_lower line 160
  15. theorem OAI.SimpleAmenable.sortedAxisCutSequence_upper line 171
  16. theorem OAI.SimpleAmenable.sortedAxisCutSequence_length line 182
  17. theorem OAI.SimpleAmenable.sortedAxisCutSequence_start line 184