OAI/GroupTheory/SimpleAmenable/PolygonGeometry/SmallFamilyWords.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.FiveAlphabet line 16
  2. abbrev OAI.SimpleAmenable.SmallFamilyLabel line 19
  3. abbrev OAI.SimpleAmenable.SmallFamilyWord line 22
  4. def OAI.SimpleAmenable.smallFamilyEval line 25
  5. theorem OAI.SimpleAmenable.smallFamilyEval_of line 29
  6. theorem OAI.SimpleAmenable.smallFamilyEval_range line 34
  7. theorem OAI.SimpleAmenable.smallFamilyEval_perfect line 49
  8. def OAI.SimpleAmenable.smallFamilyLocal line 59
  9. theorem OAI.SimpleAmenable.smallFamilyLocal_mono line 62
  10. theorem OAI.SimpleAmenable.smallFamilyLocal_of line 68
  11. theorem OAI.SimpleAmenable.smallFamilyLocal_generate line 72
  12. def OAI.SimpleAmenable.alphabetAssignment line 81
  13. theorem OAI.SimpleAmenable.alphabetAssignment_support line 87
  14. theorem OAI.SimpleAmenable.alphabetAssignment_range line 91
  15. theorem OAI.SimpleAmenable.alphabetAssignment_mask line 100
  16. def OAI.SimpleAmenable.smallFamilyModel line 109
  17. theorem OAI.SimpleAmenable.smallFamilyModel_support line 113
  18. theorem OAI.SimpleAmenable.smallFamilyModel_mask_mem line 139
  19. theorem OAI.SimpleAmenable.smallFamilyModel_complete line 159
  20. theorem OAI.SimpleAmenable.smallFamilyLocal_map_le line 177