OAI/GroupTheory/SimpleAmenable/PolygonGeometry/TangentChartTemplates.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.slopeDirection line 15
  2. def OAI.SimpleAmenable.slopeTestIndex line 16
  3. theorem OAI.SimpleAmenable.initialTest_slope line 18
  4. def OAI.SimpleAmenable.tangentOffset line 22
  5. theorem OAI.SimpleAmenable.tangentOffset_zero line 25
  6. theorem OAI.SimpleAmenable.tangentOffset_add line 28
  7. theorem OAI.SimpleAmenable.integralCutForm_tangentOffset line 32
  8. def OAI.SimpleAmenable.tangentChartTemplate line 36
  9. def OAI.SimpleAmenable.translatedTemplate line 41
  10. def OAI.SimpleAmenable.signedShortSteps line 45
  11. theorem OAI.SimpleAmenable.tangentChartTables_eventually line 47
  12. def OAI.SimpleAmenable.InitialCoverSystem.TangentChartLaws line 62
  13. def OAI.SimpleAmenable.InitialCoverSystem.tangentSign line 66
  14. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_first line 73
  15. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_second line 95
  16. theorem OAI.SimpleAmenable.integralCutForm_zero line 127
  17. theorem OAI.SimpleAmenable.integralCutForm_add line 131
  18. theorem OAI.SimpleAmenable.translatedTemplate_resolved line 135
  19. theorem OAI.SimpleAmenable.tangentChart_first_resolved line 145
  20. theorem OAI.SimpleAmenable.tangentChart_second_resolved line 155
  21. theorem OAI.SimpleAmenable.tangentChart_rectangle_resolved line 165
  22. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_step_action line 186
  23. theorem OAI.SimpleAmenable.InitialCoverSystem.tangentSign_opposite_commute line 226