OAI/GroupTheory/SimpleAmenable/Configurations/DistinctSlotStars.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.fiveAlternatingHom line 14
  2. def OAI.SimpleAmenable.orderedTrackAlphabet line 18
  3. instance OAI.SimpleAmenable.orderedTrackAlphabetPerfect line 21
  4. def OAI.SimpleAmenable.orderedTrackHom line 28
  5. theorem OAI.SimpleAmenable.orderedTrackHom_comp line 34
  6. theorem OAI.SimpleAmenable.orderedTrackAlphabet_mem line 40
  7. theorem OAI.SimpleAmenable.orderedTrackHom_apply line 43
  8. def OAI.SimpleAmenable.slotAlternatingHom line 54
  9. def OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar line 67
  10. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_apply line 73
  11. theorem OAI.SimpleAmenable.InitialCoverSystem.distinctSlotStar_projection line 87