OAI/GroupTheory/SimpleAmenable/Configurations/PolygonStringNormalization.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.PolygonObject.TrajectoryLabel line 16
  2. instance OAI.SimpleAmenable.PolygonObject.trajectoryLabel_fintype line 17
  3. def OAI.SimpleAmenable.PolygonObject.trajectoryLabel line 20
  4. theorem OAI.SimpleAmenable.PolygonObject.trajectoryLabel_fiber_polygon line 23
  5. def OAI.SimpleAmenable.PolygonObject.strandObject line 28
  6. def OAI.SimpleAmenable.PolygonObject.strandDrop line 31
  7. def OAI.SimpleAmenable.PolygonObject.strandOffsets line 34
  8. theorem OAI.SimpleAmenable.PolygonObject.strandOffsets_spec line 38
  9. def OAI.SimpleAmenable.PolygonObject.translationString line 43
  10. def OAI.SimpleAmenable.PolygonObject.normalizedString line 50
  11. def OAI.SimpleAmenable.PolygonObject.normalizationLadder line 52
  12. theorem OAI.SimpleAmenable.PolygonObject.normalizationLadder_positional line 66
  13. def OAI.SimpleAmenable.PolygonObject.normalizationIso line 77
  14. theorem OAI.SimpleAmenable.PolygonObject.exists_finite_strand_normalization line 81
  15. theorem OAI.SimpleAmenable.PolygonObject.trajectoryShift_zero line 93
  16. theorem OAI.SimpleAmenable.PolygonObject.trajectoryShift_reindex line 98
  17. def OAI.SimpleAmenable.PolygonObject.increments line 107
  18. theorem OAI.SimpleAmenable.PolygonObject.trajectory_successor line 111
  19. theorem OAI.SimpleAmenable.PolygonObject.increments_reindex line 121
  20. theorem OAI.SimpleAmenable.PolygonObject.increments_reindex_unchanged line 129
  21. theorem OAI.SimpleAmenable.PolygonObject.increments_reindex_compose line 136
  22. theorem OAI.SimpleAmenable.PolygonObject.increments_reindex_duplicate line 147
  23. theorem OAI.SimpleAmenable.PolygonObject.reindex_initial_position line 153
  24. theorem OAI.SimpleAmenable.PolygonObject.increments_finite_range line 158
  25. theorem OAI.SimpleAmenable.PolygonObject.increments_fiber_polygon line 162
  26. theorem OAI.SimpleAmenable.PolygonObject.ladder_preserves_increments line 188
  27. def OAI.SimpleAmenable.PolygonObject.deleteVertex line 194
  28. def OAI.SimpleAmenable.PolygonObject.stringFace line 197