OAI/GroupTheory/SimpleAmenable/PolygonGeometry/TupleChartDomain.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.tupleChartDomain line 13
  2. theorem OAI.SimpleAmenable.mem_tupleChartDomain line 25
  3. def OAI.SimpleAmenable.trackCycle line 36
  4. theorem OAI.SimpleAmenable.trackCycle_apply line 39
  5. theorem OAI.SimpleAmenable.trackCycle_apply_of_notMem line 44
  6. theorem OAI.SimpleAmenable.slotHom_cycle_isThreeSlotCycle line 51
  7. def OAI.SimpleAmenable.threeInFive line 78
  8. def OAI.SimpleAmenable.leftThreeInFive line 79
  9. def OAI.SimpleAmenable.rightThreeInFive line 80
  10. theorem OAI.SimpleAmenable.five_cycle_commutator line 83
  11. theorem OAI.SimpleAmenable.two_spare_tracks line 87
  12. def OAI.SimpleAmenable.extendSlots line 107
  13. theorem OAI.SimpleAmenable.extendSlots_three line 112
  14. theorem OAI.SimpleAmenable.extendSlots_injective line 117
  15. theorem OAI.SimpleAmenable.threeSlotCycle_is_commutator line 153
  16. theorem OAI.SimpleAmenable.polygonAlternatingGroup_perfect line 186
  17. theorem OAI.SimpleAmenable.conditional_isThreeSlotCycle line 197
  18. theorem OAI.SimpleAmenable.conditional_cycle_mem line 223
  19. theorem OAI.SimpleAmenable.conditional_cycle_injective line 238
  20. def OAI.SimpleAmenable.shrinkingLevel line 251
  21. theorem OAI.SimpleAmenable.ordinary_shrinkingLevel line 253
  22. theorem OAI.SimpleAmenable.shrinkingLevel_bounds line 257
  23. theorem OAI.SimpleAmenable.shrinkingLevel_strictAnti line 263
  24. def OAI.SimpleAmenable.shrinkingPolygon line 269
  25. theorem OAI.SimpleAmenable.shrinkingPolygon_injective line 272
  26. theorem OAI.SimpleAmenable.polygonAlternatingGroup_infinite line 291
  27. theorem OAI.SimpleAmenable.conjugate_threeSlot_mem line 303
  28. theorem OAI.SimpleAmenable.polygonAlternatingGroup_normal line 354
  29. theorem OAI.SimpleAmenable.isThreeCycle_eq_trackCycle line 365
  30. theorem OAI.SimpleAmenable.slotHom_alternating_mem line 380
  31. theorem OAI.SimpleAmenable.conditionalHom_alternating_mem line 398
  32. def OAI.SimpleAmenable.trackTranslationPerm line 410