OAI/GroupTheory/SimpleAmenable/CentralCovers/AssignmentGeneration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.sectorMask_inter_commutator line 17
  2. theorem OAI.SimpleAmenable.sectorMask_complement line 24
  3. def OAI.SimpleAmenable.SectorAvailable line 30
  4. theorem OAI.SimpleAmenable.sectorAvailable_inter line 33
  5. theorem OAI.SimpleAmenable.sectorAvailable_compl line 47
  6. theorem OAI.SimpleAmenable.sectorAvailable_finsetInter line 54
  7. theorem OAI.SimpleAmenable.assignment_group_generated line 66
  8. def OAI.SimpleAmenable.CommutingFactors.projectLeft line 113
  9. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_mem line 117
  10. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_factors line 121
  11. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_fix line 130
  12. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_kill line 134
  13. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_split line 138
  14. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_preserves line 146
  15. theorem OAI.SimpleAmenable.CommutingFactors.projectLeft_comp_commute line 155
  16. def OAI.SimpleAmenable.assignmentFactor line 168
  17. theorem OAI.SimpleAmenable.projectLeft_mem_assignmentFactor line 171
  18. theorem OAI.SimpleAmenable.split_assignmentFactor line 180
  19. def OAI.SimpleAmenable.refinedFactor line 190
  20. theorem OAI.SimpleAmenable.simultaneous_refinement line 194
  21. theorem OAI.SimpleAmenable.refinedFactor_commute line 229
  22. theorem OAI.SimpleAmenable.commuting_factors_independent line 243
  23. def OAI.SimpleAmenable.commutingFactorsEquiv line 275
  24. theorem OAI.SimpleAmenable.commutingFactorsEquiv_single line 286