OAI/Combinatorics/MatchingCount/Graphs/Cycle.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.cycle line 16
  2. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.cell line 19
  3. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.last_lt line 23
  4. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.corners line 29
  5. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.raw line 31
  6. theorem OAI.MatchingFPRAS.Transport.CellDemands.Demand.raw_injective line 35
  7. lemma OAI.MatchingFPRAS.Transport.OddPath.closed_eq_through_of_short line 87
  8. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellShort_chord line 104
  9. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellShort_pattern line 127
  10. instance OAI.MatchingFPRAS.Transport.CellDemands.(instance at line 147) line 147
  11. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.paths line 151
  12. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.outside line 153
  13. abbrev OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand line 157
  14. instance OAI.MatchingFPRAS.Transport.CellDemands.(instance at line 162) line 162
  15. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.bit line 168
  16. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.demand line 170
  17. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.X line 172
  18. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.Y line 174
  19. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.X_bit line 177
  20. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.Y_bit line 180
  21. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.X_ne_Y line 183
  22. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.flags line 185
  23. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.raw line 187
  24. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.raw_injective line 190
  25. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.exists_switch line 218
  26. def OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchChoice line 229
  27. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchChoice_spec line 232
  28. lemma OAI.MatchingFPRAS.Transport.CellDemands.Demand.switchChoice_injective line 242
  29. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.exists_errors line 254
  30. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.errorZero line 278
  31. def OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.errorOne line 281
  32. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.errorZero_injective line 284
  33. lemma OAI.MatchingFPRAS.Transport.CellDemands.ErrorDemand.errorOne_injective line 289
  34. def OAI.MatchingFPRAS.Transport.OddPath.closedCycle line 308
  35. lemma OAI.MatchingFPRAS.Transport.OddPath.closedCycle_edgeAt line 329
  36. lemma OAI.MatchingFPRAS.Transport.OddPath.closedCycle_chord line 335
  37. lemma OAI.MatchingFPRAS.Transport.OddPath.closedCycle_parity_zero line 340
  38. lemma OAI.MatchingFPRAS.Transport.OddPath.closedCycle_parity_one line 359
  39. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeSet_eq_parity_union line 396
  40. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.zero_mem_parity line 408
  41. abbrev OAI.MatchingFPRAS.Transport.PatternCode line 414