OAI/GroupTheory/SimpleAmenable/Configurations/RepeatedTrackRouting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SimpleAmenable.PrivateRoutingBank line 11
  2. def OAI.SimpleAmenable.PrivateRoutingBank.target line 20
  3. def OAI.SimpleAmenable.PrivateRoutingBank.alphabet line 23
  4. theorem OAI.SimpleAmenable.PrivateRoutingBank.alphabet_card line 26
  5. theorem OAI.SimpleAmenable.PrivateRoutingBank.row_subset line 30
  6. theorem OAI.SimpleAmenable.PrivateRoutingBank.source_mem line 36
  7. theorem OAI.SimpleAmenable.PrivateRoutingBank.target_other_notmem line 40
  8. theorem OAI.SimpleAmenable.PrivateRoutingBank.source_other_frame_notmem line 50
  9. theorem OAI.SimpleAmenable.exists_privateRoutingBank line 69
  10. def OAI.SimpleAmenable.InitialCoverSystem.privateRoutingFactor line 124
  11. def OAI.SimpleAmenable.InitialCoverSystem.privateRoutingWord line 132
  12. theorem OAI.SimpleAmenable.InitialCoverSystem.privateRoutingWord_properties line 138
  13. theorem OAI.SimpleAmenable.InitialCoverSystem.repeated_bank_routing line 193