OAI/Combinatorics/MatchingCount/Graphs/IndexedCycle.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MatchingFPRAS.Transport.IndexedCycle line 14
  2. def OAI.MatchingFPRAS.Transport.IndexedCycle.index line 27
  3. def OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAt line 29
  4. def OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt line 31
  5. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.index_succ line 33
  6. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAt_mod line 37
  7. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAt_periodic line 40
  8. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_incidence line 43
  9. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.mod_of_lt_twice line 47
  10. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAt_eq_iff line 53
  11. def OAI.MatchingFPRAS.Transport.IndexedCycle.arc line 63
  12. structure OAI.MatchingFPRAS.Transport.IndexedCycle.Corners line 82
  13. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.start line 100
  14. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.stop line 102
  15. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.length line 104
  16. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.bounds line 106
  17. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.length_pos line 116
  18. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.length_lt line 121
  19. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.length_odd line 126
  20. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.side line 133
  21. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.side_vertex line 137
  22. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.side_length line 140
  23. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.side_first line 142
  24. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.side_last line 145
  25. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.joins line 153
  26. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.starts_injective line 159
  27. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.corners_injective line 166
  28. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.inside_iff line 177
  29. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.interior_ranges_disjoint line 195
  30. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.interiors_disjoint line 204
  31. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.interior_not_corner_index line 219
  32. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.interior_ne_corner line 227
  33. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.interior_ends_disjoint line 238
  34. def OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cellPaths line 244
  35. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAt_mod line 269
  36. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.consecutive_ne line 272
  37. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edges_reachable line 284
  38. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.adjacent_mem_complement line 304
  39. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cycle_edge_mem_complement line 319
  40. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cycle_edge_mem_parity line 336
  41. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.parity_start line 359
  42. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cell_orientation_subset line 371
  43. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.Corners.cell_orientation_reachable line 411