OAI/Combinatorics/Ryser/Incidence/WalkCounts.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RyserCoveringCounterexample.Incidence.neighbors line 15
  2. def OAI.RyserCoveringCounterexample.Incidence.commonNeighbors line 18
  3. def OAI.RyserCoveringCounterexample.Incidence.fourWalks line 21
  4. theorem OAI.RyserCoveringCounterexample.Incidence.mem_neighbors line 25
  5. theorem OAI.RyserCoveringCounterexample.Incidence.mem_commonNeighbors line 29
  6. theorem OAI.RyserCoveringCounterexample.Incidence.mem_fourWalks line 34
  7. theorem OAI.RyserCoveringCounterexample.Incidence.neighbors_subset line 41
  8. theorem OAI.RyserCoveringCounterexample.Incidence.commonNeighbors_comm line 44
  9. theorem OAI.RyserCoveringCounterexample.Incidence.fourWalks_mono line 49
  10. theorem OAI.RyserCoveringCounterexample.Incidence.card_fourWalks line 54
  11. theorem OAI.RyserCoveringCounterexample.Incidence.card_edges_eq_sum_neighbors line 60
  12. def OAI.RyserCoveringCounterexample.Incidence.badPairs line 76
  13. def OAI.RyserCoveringCounterexample.Incidence.badPartners line 80
  14. def OAI.RyserCoveringCounterexample.Incidence.localBad line 84
  15. theorem OAI.RyserCoveringCounterexample.Incidence.mem_badPairs line 88
  16. theorem OAI.RyserCoveringCounterexample.Incidence.mem_badPartners line 94
  17. theorem OAI.RyserCoveringCounterexample.Incidence.badPartners_subset line 100
  18. theorem OAI.RyserCoveringCounterexample.Incidence.card_badPairs_eq_sum_badPartners line 104
  19. theorem OAI.RyserCoveringCounterexample.Incidence.sum_localBad_card_eq_sum_common line 109
  20. theorem OAI.RyserCoveringCounterexample.Incidence.localBad_eq_badPairs_neighbors line 116