OAI/Combinatorics/ListHadwiger/Connectivity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.exists_injective_neighborPairs line 9
  2. theorem OAI.LinearListHadwiger.high_neighbor_count line 75
  3. theorem OAI.LinearListHadwiger.choosable_add_deleted_card line 100
  4. theorem OAI.LinearListHadwiger.listChromaticNumber_deleted line 154
  5. def OAI.LinearListHadwiger.DegenerateOn line 163
  6. theorem OAI.LinearListHadwiger.degenerate_coloring_on line 166
  7. theorem OAI.LinearListHadwiger.choosable_of_degenerate line 217
  8. theorem OAI.LinearListHadwiger.listChromaticNumber_le_of_degenerate line 232