OAI/Combinatorics/MatchingCount/Graphs/ArcData.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Cells.exists_walk_on_trace line 11
  2. lemma OAI.MatchingFPRAS.Cells.neighbor_return line 35
  3. structure OAI.MatchingFPRAS.Cells.ArcData line 49
  4. def OAI.MatchingFPRAS.Cells.ArcData.Admissible line 60
  5. def OAI.MatchingFPRAS.Cells.ArcData.Good line 62
  6. structure OAI.MatchingFPRAS.Cells.ArcData.Split line 64
  7. lemma OAI.MatchingFPRAS.Cells.ArcData.trace line 79
  8. lemma OAI.MatchingFPRAS.Cells.ArcData.edge_admissible line 83
  9. lemma OAI.MatchingFPRAS.Cells.ArcData.last_mem line 86
  10. lemma OAI.MatchingFPRAS.Cells.ArcData.good_of_same_boundary line 91
  11. lemma OAI.MatchingFPRAS.Cells.ArcData.neighbor_return_between line 98
  12. lemma OAI.MatchingFPRAS.Cells.ArcData.split_short_middle line 113
  13. lemma OAI.MatchingFPRAS.Cells.ArcData.split_short_outer line 124
  14. lemma OAI.MatchingFPRAS.Cells.ArcData.split_good_exterior line 140
  15. lemma OAI.MatchingFPRAS.Cells.ArcData.split_left_boundary line 229
  16. def OAI.MatchingFPRAS.Cells.ArcData.reverse line 288
  17. lemma OAI.MatchingFPRAS.Cells.ArcData.admissible_symm line 301
  18. lemma OAI.MatchingFPRAS.Cells.ArcData.good_reverse line 305
  19. def OAI.MatchingFPRAS.Cells.ArcData.Split.unreverse line 317
  20. theorem OAI.MatchingFPRAS.Cells.ArcData.split line 351
  21. structure OAI.MatchingFPRAS.Cells.CycleData line 369