OAI/Combinatorics/ListHadwiger/Incidence.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LinearListHadwiger.Incidence.hit_pool line 10
  2. lemma OAI.LinearListHadwiger.Incidence.star_connected line 43
  3. lemma OAI.LinearListHadwiger.Incidence.fresh_star line 57
  4. structure OAI.LinearListHadwiger.Incidence.BoundedBags line 121
  5. lemma OAI.LinearListHadwiger.Incidence.BoundedBags.minor line 128
  6. lemma OAI.LinearListHadwiger.Incidence.BoundedBags.succ line 133
  7. theorem OAI.LinearListHadwiger.Incidence.near_complete_minor line 155
  8. theorem OAI.LinearListHadwiger.Incidence.missing_vertex line 195
  9. def OAI.LinearListHadwiger.Incidence.addStar line 226
  10. lemma OAI.LinearListHadwiger.Incidence.addStar_le line 239
  11. lemma OAI.LinearListHadwiger.Incidence.addStar_edges line 242
  12. lemma OAI.LinearListHadwiger.Incidence.connected_insert line 270
  13. def OAI.LinearListHadwiger.Incidence.extendModel line 282
  14. lemma OAI.LinearListHadwiger.Incidence.missing_in_set line 320
  15. lemma OAI.LinearListHadwiger.Incidence.filter_subtype_card line 347
  16. theorem OAI.LinearListHadwiger.Incidence.incidence_model line 356
  17. theorem OAI.LinearListHadwiger.Incidence.incidence_finite line 422
  18. lemma OAI.LinearListHadwiger.Incidence.incidence_cutoff line 444
  19. theorem OAI.LinearListHadwiger.Incidence.incidence_bound line 488