OAI/GroupTheory/SimpleAmenable/PolygonGeometry/PolygonObjectSum.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.PolygonObject.arrow_id_apply line 15
  2. theorem OAI.SimpleAmenable.PolygonObject.arrow_comp_apply line 16
  3. def OAI.SimpleAmenable.PolygonObject.sum line 19
  4. def OAI.SimpleAmenable.PolygonObject.sumPointEquiv line 22
  5. theorem OAI.SimpleAmenable.PolygonObject.sumPointEquiv_inl line 37
  6. theorem OAI.SimpleAmenable.PolygonObject.sumPointEquiv_inr line 39
  7. theorem OAI.SimpleAmenable.PolygonObject.positional_hasTable line 42
  8. def OAI.SimpleAmenable.PolygonObject.sumArrow line 59
  9. theorem OAI.SimpleAmenable.PolygonObject.sumArrow_inl line 104
  10. theorem OAI.SimpleAmenable.PolygonObject.sumArrow_inr line 108
  11. theorem OAI.SimpleAmenable.PolygonObject.sumArrow_id line 113
  12. theorem OAI.SimpleAmenable.PolygonObject.sumArrow_comp line 118
  13. def OAI.SimpleAmenable.PolygonObject.complement line 132
  14. def OAI.SimpleAmenable.PolygonObject.splitPointEquiv line 135
  15. theorem OAI.SimpleAmenable.PolygonObject.splitPointEquiv_inl line 147
  16. theorem OAI.SimpleAmenable.PolygonObject.splitPointEquiv_inr line 149
  17. def OAI.SimpleAmenable.PolygonObject.complementArrow line 152
  18. theorem OAI.SimpleAmenable.PolygonObject.complementArrow_inl line 179
  19. theorem OAI.SimpleAmenable.PolygonObject.complementArrow_inr line 183
  20. theorem OAI.SimpleAmenable.PolygonObject.complementArrow_positional line 188
  21. def OAI.SimpleAmenable.PolygonObject.complementIso line 193