OAI/Combinatorics/ListHadwiger/Routing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.avoidingConnection_of_kConnectedOn line 9
  2. theorem OAI.LinearListHadwiger.packing_of_kConnectedOn line 36
  3. def OAI.LinearListHadwiger.deletedFibers line 45
  4. lemma OAI.LinearListHadwiger.deletedFibers_card line 50
  5. lemma OAI.LinearListHadwiger.avoiding_walk_comap line 63
  6. lemma OAI.LinearListHadwiger.packing_in_comap line 118
  7. lemma OAI.LinearListHadwiger.PathPacking.FullPacking.target_injective line 139
  8. structure OAI.LinearListHadwiger.DoublePacking line 149
  9. theorem OAI.LinearListHadwiger.double_packing line 158
  10. structure OAI.LinearListHadwiger.MinorModel line 265