OAI/GroupTheory/SimpleAmenable/PolygonGeometry/AxisCutSequences.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.AxisCutSequence line 15
  2. def OAI.SimpleAmenable.AxisCutSequence.index line 28
  3. theorem OAI.SimpleAmenable.AxisCutSequence.index_zero line 29
  4. theorem OAI.SimpleAmenable.AxisCutSequence.index_fin line 30
  5. theorem OAI.SimpleAmenable.AxisCutSequence.index_mono line 32
  6. theorem OAI.SimpleAmenable.AxisCutSequence.ordered line 36
  7. theorem OAI.SimpleAmenable.AxisCutSequence.length_old line 40
  8. def OAI.SimpleAmenable.AxisCutSequence.anchorCopy line 47
  9. def OAI.SimpleAmenable.AxisCutSequence.prefixCopy line 52
  10. def OAI.SimpleAmenable.AxisCutSequence.suffix line 57
  11. theorem OAI.SimpleAmenable.AxisCutSequence.anchorCopy_eq line 62
  12. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_suffix line 69
  13. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_zero line 76
  14. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_last line 79
  15. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_projection line 84
  16. theorem OAI.SimpleAmenable.AxisCutSequence.suffix_projection line 90
  17. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_small_supported line 96
  18. theorem OAI.SimpleAmenable.AxisCutSequence.anchorCopy_small_supported line 101
  19. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_small_controlled line 105
  20. theorem OAI.SimpleAmenable.AxisCutSequence.prefix_suffix_self_commute line 111
  21. theorem OAI.SimpleAmenable.cutDifference_small_supported line 129
  22. theorem OAI.SimpleAmenable.cutDifference_small_controlled line 137