OAI/Combinatorics/ListHadwiger/Knitting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.Knitting.connected_induce_congr line 10
  2. lemma OAI.LinearListHadwiger.Knitting.delete_connected line 14
  3. theorem OAI.LinearListHadwiger.Knitting.packing_from_many_neighbors line 34
  4. theorem OAI.LinearListHadwiger.Knitting.short_path line 67
  5. lemma OAI.LinearListHadwiger.Knitting.min_degree line 118
  6. lemma OAI.LinearListHadwiger.Knitting.induce_connected line 144
  7. lemma OAI.LinearListHadwiger.Knitting.connected_of_kConnected line 173
  8. theorem OAI.LinearListHadwiger.Knitting.short_avoiding_path line 178
  9. def OAI.LinearListHadwiger.Knitting.packedBranch line 210
  10. lemma OAI.LinearListHadwiger.Knitting.packedBranch_target line 214
  11. lemma OAI.LinearListHadwiger.Knitting.packedBranch_source line 217
  12. lemma OAI.LinearListHadwiger.Knitting.packedBranch_connected line 221
  13. lemma OAI.LinearListHadwiger.Knitting.packedBranch_disjoint line 247
  14. def OAI.LinearListHadwiger.Knitting.absorb_packing line 263
  15. def OAI.LinearListHadwiger.Knitting.compose_model line 272
  16. theorem OAI.LinearListHadwiger.Knitting.root_minor_core line 283
  17. theorem OAI.LinearListHadwiger.Knitting.group_small_core line 408