OAI/Combinatorics/ListHadwiger/ConnectivityTests.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching line 13
  2. def OAI.LinearListHadwiger.ConnectivityTests.endpoints line 17
  3. lemma OAI.LinearListHadwiger.ConnectivityTests.endpoints_card_le line 20
  4. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.mono line 26
  5. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.fst_card line 30
  6. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.snd_card line 37
  7. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.endpoints_inter_left line 44
  8. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.endpoints_inter_right line 57
  9. lemma OAI.LinearListHadwiger.ConnectivityTests.cross_edge_of_connected line 71
  10. lemma OAI.LinearListHadwiger.ConnectivityTests.crossing_edge_avoiding line 88
  11. theorem OAI.LinearListHadwiger.ConnectivityTests.exists_cut_matching line 110
  12. theorem OAI.LinearListHadwiger.ConnectivityTests.finite_hitting line 151
  13. lemma OAI.LinearListHadwiger.ConnectivityTests.sum_uniform_mask line 205
  14. theorem OAI.LinearListHadwiger.ConnectivityTests.exists_neighborhood_cover line 215
  15. lemma OAI.LinearListHadwiger.ConnectivityTests.sum_powers_le line 304
  16. def OAI.LinearListHadwiger.ConnectivityTests.smallSets line 313
  17. lemma OAI.LinearListHadwiger.ConnectivityTests.mem_smallSets line 316
  18. lemma OAI.LinearListHadwiger.ConnectivityTests.smallSets_card_le line 323
  19. lemma OAI.LinearListHadwiger.ConnectivityTests.IsCutMatching.card_le_cover line 335
  20. lemma OAI.LinearListHadwiger.ConnectivityTests.separator_neighbors_le line 363
  21. lemma OAI.LinearListHadwiger.ConnectivityTests.SeparatorSplit.swap_test line 377
  22. def OAI.LinearListHadwiger.ConnectivityTests.neighborhoodUnion line 385
  23. lemma OAI.LinearListHadwiger.ConnectivityTests.mem_neighborhoodUnion line 388
  24. theorem OAI.LinearListHadwiger.ConnectivityTests.separator_test line 393
  25. theorem OAI.LinearListHadwiger.ConnectivityTests.cut_test line 488