OAI/Combinatorics/ListHadwiger/RoleRouting.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LinearListHadwiger.Stage.RoleRouting line 9
  2. lemma OAI.LinearListHadwiger.Stage.RoleRouting.start_injective line 28
  3. lemma OAI.LinearListHadwiger.Stage.RoleRouting.target_injective line 36
  4. theorem OAI.LinearListHadwiger.Stage.RoleRouting.of_paired line 43
  5. theorem OAI.LinearListHadwiger.Stage.RoleRouting.weave line 102
  6. theorem OAI.LinearListHadwiger.Stage.combine_systems line 144
  7. lemma OAI.LinearListHadwiger.Stage.Second.used_inter_region line 203
  8. lemma OAI.LinearListHadwiger.Stage.Second.starts_card line 215
  9. lemma OAI.LinearListHadwiger.Stage.union_connected line 225
  10. def OAI.LinearListHadwiger.Stage.attached line 254
  11. def OAI.LinearListHadwiger.Stage.extended line 258
  12. lemma OAI.LinearListHadwiger.Stage.attached_connected line 262
  13. lemma OAI.LinearListHadwiger.Stage.extended_connected line 269
  14. lemma OAI.LinearListHadwiger.Stage.extended_disjoint line 290
  15. lemma OAI.LinearListHadwiger.Stage.satellite_subset line 315
  16. lemma OAI.LinearListHadwiger.Stage.path_subset line 321
  17. lemma OAI.LinearListHadwiger.Stage.extended_subset line 327
  18. theorem OAI.LinearListHadwiger.Stage.grouped_ends line 344