OAI/GroupTheory/SimpleAmenable/CentralCovers/FiniteSlotRefinement.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SimpleAmenable.polygon_finite_cover_induction line 16
  2. theorem OAI.SimpleAmenable.polygon_mem_finset_inf line 47
  3. theorem OAI.SimpleAmenable.finite_slot_chart_cover line 60
  4. theorem OAI.SimpleAmenable.SlotMap_injective_of_transport line 108
  5. def OAI.SimpleAmenable.InitialCoverSystem.ExactSlotTransport line 128
  6. def OAI.SimpleAmenable.InitialCoverSystem.UniformSlotTransport line 136
  7. theorem OAI.SimpleAmenable.InitialCoverSystem.exactSlotTransport_empty line 149
  8. theorem OAI.SimpleAmenable.InitialCoverSystem.exactSlotTransport_union line 157
  9. theorem OAI.SimpleAmenable.InitialCoverSystem.exactSlotTransport_cover line 175
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.uniformSlotTransport_one line 191
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.uniformSlotTransport_inv line 202
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.uniformSlotTransport_mul line 222
  13. def OAI.SimpleAmenable.InitialCoverSystem.slotTransportSubgroup line 263