OAI/GroupTheory/SimpleAmenable/CentralCovers/CanonicalSlotStars.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SimpleAmenable.InitialCoverSystem.SlotRouting.restrict line 18
2. def OAI.SimpleAmenable.InitialCoverSystem.SlotRouting.identity line 34
3. theorem OAI.SimpleAmenable.InitialCoverSystem.SlotRouting.identity_star line 51
4. theorem OAI.SimpleAmenable.InitialCoverSystem.SlotRouting.star_union line 60
5. theorem OAI.SimpleAmenable.InitialCoverSystem.SlotRouting.star_commute line 72
6. def OAI.SimpleAmenable.InitialCoverSystem.slotStar line 82
7. theorem OAI.SimpleAmenable.InitialCoverSystem.slotStar_eq_routing line 97
8. theorem OAI.SimpleAmenable.InitialCoverSystem.slotStar_distinct line 104
9. theorem OAI.SimpleAmenable.InitialCoverSystem.slotStar_aligned_transport line 113
10. theorem OAI.SimpleAmenable.InitialCoverSystem.slotStar_union line 128
11. theorem OAI.SimpleAmenable.InitialCoverSystem.slotStar_commute line 141