OAI/GroupTheory/SimpleAmenable/Amenability/PartitionArrows.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SimpleAmenable.TrackPolygonPartition line 15
  2. abbrev OAI.SimpleAmenable.PartitionCell line 16
  3. def OAI.SimpleAmenable.partitionCellSet line 18
  4. theorem OAI.SimpleAmenable.partitionCellSet_nonempty line 21
  5. theorem OAI.SimpleAmenable.partitionCellSet_cover line 26
  6. theorem OAI.SimpleAmenable.partitionCellSet_eq_of_mem line 37
  7. def OAI.SimpleAmenable.PartitionArrow line 42
  8. theorem OAI.SimpleAmenable.PartitionArrow.one line 50
  9. theorem OAI.SimpleAmenable.PartitionArrow.mul line 59
  10. theorem OAI.SimpleAmenable.PartitionArrow.inv line 72