OAI/GroupTheory/SimpleAmenable/Configurations/PolygonGroupoid.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.PolygonObject line 11
  2. abbrev OAI.SimpleAmenable.PolygonObject.Point line 18
  3. structure OAI.SimpleAmenable.PolygonObject.Chart line 20
  4. def OAI.SimpleAmenable.PolygonObject.Chart.Holds line 29
  5. def OAI.SimpleAmenable.PolygonObject.Chart.Contains line 33
  6. def OAI.SimpleAmenable.PolygonObject.Chart.comp line 36
  7. theorem OAI.SimpleAmenable.PolygonObject.Chart.comp_holds line 42
  8. def OAI.SimpleAmenable.PolygonObject.Chart.inverse line 56
  9. theorem OAI.SimpleAmenable.PolygonObject.Chart.inverse_holds line 61
  10. def OAI.SimpleAmenable.PolygonObject.HasTable line 78
  11. theorem OAI.SimpleAmenable.PolygonObject.identity_hasTable line 82
  12. theorem OAI.SimpleAmenable.PolygonObject.comp_hasTable line 92
  13. theorem OAI.SimpleAmenable.PolygonObject.inverse_hasTable line 120
  14. structure OAI.SimpleAmenable.PolygonObject.Arrow line 138
  15. theorem OAI.SimpleAmenable.PolygonObject.Arrow.ext line 142
  16. instance OAI.SimpleAmenable.PolygonObject.(instance at line 146) line 146
  17. def OAI.SimpleAmenable.PolygonObject.Positional line 157
  18. def OAI.SimpleAmenable.PolygonObject.positionalSubgroupoid line 160
  19. theorem OAI.SimpleAmenable.PolygonObject.identity_positional line 171