OAI/GroupTheory/SimpleAmenable/Configurations/PolygonTrajectoryStrata.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.PolygonObject.representative_add line 19
  2. theorem OAI.SimpleAmenable.PolygonObject.representative_idem line 23
  3. theorem OAI.SimpleAmenable.PolygonObject.arrow_displacement_exists line 27
  4. def OAI.SimpleAmenable.PolygonObject.pointShift line 37
  5. theorem OAI.SimpleAmenable.PolygonObject.pointShift_spec line 40
  6. theorem OAI.SimpleAmenable.PolygonObject.pointShift_unique line 44
  7. theorem OAI.SimpleAmenable.PolygonObject.pointShift_reduced line 50
  8. theorem OAI.SimpleAmenable.PolygonObject.pointShift_id line 53
  9. theorem OAI.SimpleAmenable.PolygonObject.pointShift_comp line 57
  10. theorem OAI.SimpleAmenable.PolygonObject.chart_pointShift line 63
  11. theorem OAI.SimpleAmenable.PolygonObject.pointShift_finite_range line 72
  12. theorem OAI.SimpleAmenable.PolygonObject.pointShift_fiber_polygon line 80
  13. def OAI.SimpleAmenable.PolygonObject.trajectoryShift line 104
  14. theorem OAI.SimpleAmenable.PolygonObject.trajectoryShift_fiber_polygon line 107
  15. theorem OAI.SimpleAmenable.PolygonObject.trajectoryShift_finite_range line 126
  16. theorem OAI.SimpleAmenable.PolygonObject.ladder_preserves_trajectoryShift line 136
  17. theorem OAI.SimpleAmenable.PolygonObject.trajectory_stratification line 151