OAI/Combinatorics/ListHadwiger/Footprint.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.LinearListHadwiger.Footprint.degenerate_of_phases line 9
  2. theorem OAI.LinearListHadwiger.Footprint.neighbors_in_collection line 35
  3. theorem OAI.LinearListHadwiger.Footprint.collection_incidence line 58
  4. theorem OAI.LinearListHadwiger.Footprint.minimum_system_degenerate line 124
  5. theorem OAI.LinearListHadwiger.Footprint.minimum_system_path_neighbors line 151
  6. def OAI.LinearListHadwiger.Footprint.exceptional line 166
  7. theorem OAI.LinearListHadwiger.Footprint.exceptional_card line 171
  8. theorem OAI.LinearListHadwiger.Footprint.path_erase_start_connected line 198
  9. theorem OAI.LinearListHadwiger.Footprint.stripped_disjoint line 215
  10. def OAI.LinearListHadwiger.Footprint.rounds line 231
  11. lemma OAI.LinearListHadwiger.Footprint.rounds_le_log line 233
  12. lemma OAI.LinearListHadwiger.Footprint.exceptional_size_cutoff line 250
  13. structure OAI.LinearListHadwiger.Footprint.System line 297
  14. def OAI.LinearListHadwiger.Footprint.System.path line 307
  15. def OAI.LinearListHadwiger.Footprint.System.used line 309
  16. def OAI.LinearListHadwiger.Footprint.System.starts line 310
  17. def OAI.LinearListHadwiger.Footprint.System.ends line 311
  18. def OAI.LinearListHadwiger.Footprint.System.stripped line 313
  19. lemma OAI.LinearListHadwiger.Footprint.System.path_subset_domain line 316
  20. lemma OAI.LinearListHadwiger.Footprint.System.mem_used line 321
  21. lemma OAI.LinearListHadwiger.Footprint.System.used_eq line 325
  22. lemma OAI.LinearListHadwiger.Footprint.System.path_subset_used line 329
  23. lemma OAI.LinearListHadwiger.Footprint.System.used_subset_domain line 332
  24. lemma OAI.LinearListHadwiger.Footprint.System.start_mem_path line 337
  25. lemma OAI.LinearListHadwiger.Footprint.System.end_mem_path line 340
  26. lemma OAI.LinearListHadwiger.Footprint.System.starts_card line 343
  27. lemma OAI.LinearListHadwiger.Footprint.System.ends_card line 346
  28. lemma OAI.LinearListHadwiger.Footprint.System.overlap line 349
  29. lemma OAI.LinearListHadwiger.Footprint.System.start_on_path line 359
  30. lemma OAI.LinearListHadwiger.Footprint.System.stripped_disjoint line 366
  31. lemma OAI.LinearListHadwiger.Footprint.System.paths_disjoint line 373
  32. lemma OAI.LinearListHadwiger.Footprint.System.degenerate line 380
  33. lemma OAI.LinearListHadwiger.Footprint.System.path_neighbors line 384
  34. lemma OAI.LinearListHadwiger.Footprint.System.used_neighbors line 389
  35. lemma OAI.LinearListHadwiger.Footprint.System.path_connected line 395
  36. lemma OAI.LinearListHadwiger.Footprint.System.stripped_connected line 407