OAI/Combinatorics/ListHadwiger/History.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LinearListHadwiger.Footprint.History line 9
  2. lemma OAI.LinearListHadwiger.Footprint.History.step_subset line 43
  3. lemma OAI.LinearListHadwiger.Footprint.History.footprint_mono line 49
  4. lemma OAI.LinearListHadwiger.Footprint.History.first_used_next line 56
  5. lemma OAI.LinearListHadwiger.Footprint.History.second_used_next line 61
  6. lemma OAI.LinearListHadwiger.Footprint.History.district_next line 66
  7. lemma OAI.LinearListHadwiger.Footprint.History.roots_next line 71
  8. lemma OAI.LinearListHadwiger.Footprint.History.first_stripped_avoids line 74
  9. lemma OAI.LinearListHadwiger.Footprint.History.second_avoids line 87
  10. abbrev OAI.LinearListHadwiger.Footprint.History.FirstIndex line 95
  11. abbrev OAI.LinearListHadwiger.Footprint.History.SecondIndex line 96
  12. def OAI.LinearListHadwiger.Footprint.History.firstPath line 97
  13. def OAI.LinearListHadwiger.Footprint.History.secondPath line 99
  14. lemma OAI.LinearListHadwiger.Footprint.History.firstPath_next line 102
  15. lemma OAI.LinearListHadwiger.Footprint.History.secondPath_next line 106
  16. lemma OAI.LinearListHadwiger.Footprint.History.firstPath_connected line 110
  17. lemma OAI.LinearListHadwiger.Footprint.History.secondPath_connected line 125
  18. lemma OAI.LinearListHadwiger.Footprint.History.firstPath_disjoint line 128
  19. lemma OAI.LinearListHadwiger.Footprint.History.secondPath_disjoint line 143
  20. lemma OAI.LinearListHadwiger.Footprint.History.firstIndex_card line 158
  21. lemma OAI.LinearListHadwiger.Footprint.History.secondIndex_card line 164
  22. abbrev OAI.LinearListHadwiger.Footprint.History.FirstPast line 178
  23. abbrev OAI.LinearListHadwiger.Footprint.History.SecondPast line 179
  24. lemma OAI.LinearListHadwiger.Footprint.History.firstPast_subset line 181
  25. lemma OAI.LinearListHadwiger.Footprint.History.secondPast_subset line 185
  26. lemma OAI.LinearListHadwiger.Footprint.History.firstPast_card line 189
  27. lemma OAI.LinearListHadwiger.Footprint.History.secondPast_card line 192
  28. def OAI.LinearListHadwiger.Footprint.History.firstException line 195
  29. def OAI.LinearListHadwiger.Footprint.History.secondException line 197
  30. lemma OAI.LinearListHadwiger.Footprint.History.exceptions_card line 200
  31. def OAI.LinearListHadwiger.Footprint.History.small line 235
  32. lemma OAI.LinearListHadwiger.Footprint.History.small_round_card line 240
  33. lemma OAI.LinearListHadwiger.Footprint.History.small_card line 269
  34. def OAI.LinearListHadwiger.Footprint.History.deleted line 288
  35. lemma OAI.LinearListHadwiger.Footprint.History.deleted_card line 291
  36. lemma OAI.LinearListHadwiger.Footprint.degenerate_union line 319
  37. lemma OAI.LinearListHadwiger.Footprint.History.initial_small line 345
  38. lemma OAI.LinearListHadwiger.Footprint.History.round_small line 347
  39. lemma OAI.LinearListHadwiger.Footprint.History.district_small line 353
  40. lemma OAI.LinearListHadwiger.Footprint.History.junction_small line 356
  41. lemma OAI.LinearListHadwiger.Footprint.History.first_starts_small line 359
  42. lemma OAI.LinearListHadwiger.Footprint.History.small_deleted line 363
  43. lemma OAI.LinearListHadwiger.Footprint.History.footprint_path line 365
  44. lemma OAI.LinearListHadwiger.Footprint.History.first_exception_deleted line 394
  45. lemma OAI.LinearListHadwiger.Footprint.History.second_exception_deleted line 398
  46. lemma OAI.LinearListHadwiger.Footprint.History.first_nonexceptional line 403
  47. lemma OAI.LinearListHadwiger.Footprint.History.second_nonexceptional line 410
  48. lemma OAI.LinearListHadwiger.Footprint.History.first_past_neighbors line 418
  49. lemma OAI.LinearListHadwiger.Footprint.History.second_past_neighbors line 432
  50. lemma OAI.LinearListHadwiger.Footprint.History.past_neighbors line 448