OAI/Combinatorics/MatchingCount/Graphs/Sets.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Cells.CycleData.sets line 15
  2. def OAI.MatchingFPRAS.Cells.CycleData.Admissible line 17
  3. def OAI.MatchingFPRAS.Cells.CycleData.Good line 19
  4. def OAI.MatchingFPRAS.Cells.CycleData.ExteriorGood line 21
  5. lemma OAI.MatchingFPRAS.Cells.CycleData.sets_clique line 24
  6. def OAI.MatchingFPRAS.Cells.CycleData.arc line 33
  7. lemma OAI.MatchingFPRAS.Cells.CycleData.arc_admissible line 45
  8. lemma OAI.MatchingFPRAS.Cells.CycleData.arc_good line 49
  9. lemma OAI.MatchingFPRAS.Cells.CycleData.bad_exterior_boundary line 63
  10. structure OAI.MatchingFPRAS.Cells.CycleData.Cell line 95
  11. inductive OAI.MatchingFPRAS.Cells.CycleData.Subdivision line 111
  12. lemma OAI.MatchingFPRAS.Cells.CycleData.cell_of_split line 117
  13. theorem OAI.MatchingFPRAS.Cells.CycleData.quadrangulate_arc line 150
  14. theorem OAI.MatchingFPRAS.Cells.CycleData.quadrangulate line 181
  15. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cells line 202
  16. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.leaves line 206
  17. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.cells_length line 210
  18. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.leaves_length line 215
  19. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.interiorDiagonals line 220
  20. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.counts line 222
  21. def OAI.MatchingFPRAS.Cells.CycleData.Subdivision.sumCells line 230
  22. lemma OAI.MatchingFPRAS.Cells.CycleData.Subdivision.signed_cancellation line 235
  23. def OAI.MatchingFPRAS.Transport.IndexedCycle.zindex line 260
  24. def OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAtZ line 264
  25. def OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAtZ line 266
  26. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.zindex_nat line 268
  27. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.zindex_periodic line 273
  28. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAtZ_nat line 277
  29. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAtZ_nat line 280
  30. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.vertexAtZ_periodic line 283
  31. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAtZ_periodic line 286
  32. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.zindex_succ line 289
  33. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edgeAtZ_incidence line 300
  34. def OAI.MatchingFPRAS.Transport.BagEdge.color line 310
  35. lemma OAI.MatchingFPRAS.Transport.BagEdge.color_mem line 312
  36. def OAI.MatchingFPRAS.Transport.BagEdge.ofEndpoints line 315
  37. lemma OAI.MatchingFPRAS.Transport.BagEdge.ofEndpoints_incidence line 325
  38. lemma OAI.MatchingFPRAS.Transport.BagEdge.ofEndpoints_color line 330