OAI/GroupTheory/SimpleAmenable/Configurations/TrackPoint.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.TrackPoint line 14
  2. structure OAI.SimpleAmenable.TableChart line 16
  3. def OAI.SimpleAmenable.TableChart.Holds line 22
  4. def OAI.SimpleAmenable.TableChart.Contains line 25
  5. def OAI.SimpleAmenable.HasTranslationTable line 28
  6. def OAI.SimpleAmenable.identityChart line 32
  7. theorem OAI.SimpleAmenable.identity_hasTable line 35
  8. def OAI.SimpleAmenable.TableChart.comp line 46
  9. theorem OAI.SimpleAmenable.TableChart.comp_holds line 51
  10. theorem OAI.SimpleAmenable.comp_hasTable line 59
  11. def OAI.SimpleAmenable.TableChart.inverse line 85
  12. theorem OAI.SimpleAmenable.inverse_hasTable line 89
  13. def OAI.SimpleAmenable.polygonFullGroup line 111
  14. def OAI.SimpleAmenable.SlotMap line 117
  15. def OAI.SimpleAmenable.IsThreeSlotCycle line 122
  16. def OAI.SimpleAmenable.polygonAlternatingGroup line 129
  17. def OAI.SimpleAmenable.conditionalPerm line 132
  18. theorem OAI.SimpleAmenable.conditionalPerm_apply line 141
  19. def OAI.SimpleAmenable.conditionalChart line 147
  20. theorem OAI.SimpleAmenable.conditional_hasTable line 152
  21. def OAI.SimpleAmenable.conditionalHom line 172
  22. def OAI.SimpleAmenable.slotPerm line 188
  23. theorem OAI.SimpleAmenable.slotPerm_apply line 194
  24. theorem OAI.SimpleAmenable.slotPerm_apply_of_notMem line 202
  25. def OAI.SimpleAmenable.slotChart line 209
  26. def OAI.SimpleAmenable.slotVoid line 215
  27. theorem OAI.SimpleAmenable.slotVoid_mem line 220
  28. theorem OAI.SimpleAmenable.mem_slotVoid line 230
  29. def OAI.SimpleAmenable.slotVoidChart line 242
  30. theorem OAI.SimpleAmenable.slotPerm_hasTable line 246
  31. def OAI.SimpleAmenable.slotHom line 280
  32. theorem OAI.SimpleAmenable.SlotMap_injective_mono line 304
  33. def OAI.SimpleAmenable.polygonInter line 314
  34. def OAI.SimpleAmenable.polygonDiff line 317
  35. theorem OAI.SimpleAmenable.slotPerm_restrict_apply line 320
  36. theorem OAI.SimpleAmenable.slotHom_split line 336
  37. theorem OAI.SimpleAmenable.slotHom_empty line 367
  38. theorem OAI.SimpleAmenable.slotHom_of_finite_cover line 378
  39. theorem OAI.SimpleAmenable.slotHom_conjugate line 410