OAI/GroupTheory/SimpleAmenable/Configurations/TrajectoryLabels.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.PolygonObject.Labelled line 9
  2. structure OAI.SimpleAmenable.PolygonObject.Labelled.Hom line 16
  3. theorem OAI.SimpleAmenable.PolygonObject.Labelled.Hom.ext line 21
  4. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 24) line 24
  5. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 33) line 33
  6. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 41) line 41
  7. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.string line 43
  8. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.initial line 45
  9. def OAI.SimpleAmenable.PolygonObject.Labelled.initialArrow line 47
  10. theorem OAI.SimpleAmenable.PolygonObject.Labelled.initialArrow_positional line 51
  11. theorem OAI.SimpleAmenable.PolygonObject.Labelled.initialArrow_labelled line 56
  12. def OAI.SimpleAmenable.PolygonObject.Labelled.ladder line 64
  13. theorem OAI.SimpleAmenable.PolygonObject.Labelled.ladder_zero line 68
  14. def OAI.SimpleAmenable.PolygonObject.Labelled.toStrings line 71
  15. def OAI.SimpleAmenable.PolygonObject.Labelled.fromLadder line 89
  16. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 101) line 101
  17. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 109) line 109
  18. theorem OAI.SimpleAmenable.PolygonObject.Labelled.increments_reduced line 117
  19. abbrev OAI.SimpleAmenable.PolygonObject.Labelled.Support line 121
  20. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 122) line 122
  21. def OAI.SimpleAmenable.PolygonObject.Labelled.supportLabel line 124
  22. theorem OAI.SimpleAmenable.PolygonObject.Labelled.supportLabel_polygon line 126
  23. def OAI.SimpleAmenable.PolygonObject.Labelled.refine line 130
  24. def OAI.SimpleAmenable.PolygonObject.Labelled.drop line 138
  25. theorem OAI.SimpleAmenable.PolygonObject.Labelled.drop_label line 141
  26. def OAI.SimpleAmenable.PolygonObject.Labelled.refinementLadder line 145
  27. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 155) line 155
  28. instance OAI.SimpleAmenable.PolygonObject.Labelled.(instance at line 160) line 160
  29. def OAI.SimpleAmenable.PolygonObject.Labelled.equivalence line 162