OAI/GroupTheory/SimpleAmenable/CentralCovers/BoundedRelationCover.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.ShortWord line 13
  2. def OAI.SimpleAmenable.ShortWord.value line 15
  3. instance OAI.SimpleAmenable.(instance at line 18) line 18
  4. def OAI.SimpleAmenable.shortRelations line 24
  5. theorem OAI.SimpleAmenable.shortRelations_finite line 27
  6. abbrev OAI.SimpleAmenable.BoundedRelationCover line 30
  7. instance OAI.SimpleAmenable.(instance at line 32) line 32
  8. def OAI.SimpleAmenable.coverMap line 37
  9. theorem OAI.SimpleAmenable.coverMap_mk line 40
  10. theorem OAI.SimpleAmenable.coverMap_of line 43
  11. theorem OAI.SimpleAmenable.coverMap_surjective line 47
  12. theorem OAI.SimpleAmenable.mem_shortRelations_of_length line 53
  13. theorem OAI.SimpleAmenable.finite_true_relations_bounded line 62
  14. theorem OAI.SimpleAmenable.finite_table_lift line 71
  15. theorem OAI.SimpleAmenable.finitelyPresented_of_cover line 99
  16. theorem OAI.SimpleAmenable.shortRelations_mono line 110
  17. def OAI.SimpleAmenable.coverTransition line 115
  18. theorem OAI.SimpleAmenable.coverTransition_mk line 119
  19. theorem OAI.SimpleAmenable.coverTransition_surjective line 123
  20. theorem OAI.SimpleAmenable.coverTransition_projection line 129
  21. theorem OAI.SimpleAmenable.finite_table_lift_eventually line 134
  22. theorem OAI.SimpleAmenable.bounded_cover_eventually_perfect line 145
  23. theorem OAI.SimpleAmenable.finitelyPresented_lift_eventually line 181