OAI/Combinatorics/ListHadwiger/PathPacking.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.PathPacking.AvoidingConnection line 9
  2. theorem OAI.LinearListHadwiger.PathPacking.successor_of_no_small_separator line 12
  3. def OAI.LinearListHadwiger.PathPacking.next line 90
  4. lemma OAI.LinearListHadwiger.PathPacking.next_not_source line 92
  5. lemma OAI.LinearListHadwiger.PathPacking.next_injective_off_target line 96
  6. lemma OAI.LinearListHadwiger.PathPacking.orbit_collision line 103
  7. lemma OAI.LinearListHadwiger.PathPacking.orbit_hits_target line 131
  8. lemma OAI.LinearListHadwiger.PathPacking.orbit_walk line 144
  9. structure OAI.LinearListHadwiger.PathPacking.FullPacking line 179
  10. theorem OAI.LinearListHadwiger.PathPacking.fullPacking_of_successor line 187
  11. theorem OAI.LinearListHadwiger.PathPacking.fullPacking_of_no_small_separator line 228