OAI/Combinatorics/MatchingCount/Graphs/LabelCycle.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.current_color_mem line 18
  2. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.previous_color_mem line 21
  3. def OAI.MatchingFPRAS.Transport.IndexedCycle.labelCycle line 28
  4. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.labelCycle_sets_subset line 35
  5. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.admissible_common_bag line 43
  6. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.labelSets_periodic line 50
  7. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.edge_color_fixed line 55
  8. def OAI.MatchingFPRAS.Transport.IndexedCycle.chord line 63
  9. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.chord_incidence line 78
  10. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.chord_short line 93
  11. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.chord_wrap line 98
  12. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.chord_color_fixed line 104
  13. def OAI.MatchingFPRAS.Transport.IndexedCycle.cellCorners line 119
  14. def OAI.MatchingFPRAS.Transport.IndexedCycle.cellChords line 137
  15. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellChords_incidence line 145
  16. def OAI.MatchingFPRAS.Transport.IndexedCycle.pathsOfCell line 157
  17. def OAI.MatchingFPRAS.Transport.IndexedCycle.sideGood line 162
  18. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cell_sideGood line 166
  19. def OAI.MatchingFPRAS.Transport.IndexedCycle.leafRepair line 187
  20. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.leafRepair_incidence line 218
  21. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.leafRepair_color_fixed line 224
  22. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cell_has_good_pair line 231
  23. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cell_actual_repairs line 245
  24. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cell_long_opposite_good line 254
  25. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellChords_fixed line 279
  26. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellChords_previous_fixed line 298
  27. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.fixed_height_ratio line 316
  28. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cellChords_height_ratio line 324
  29. def OAI.MatchingFPRAS.Transport.IndexedCycle.LocalEdge line 359
  30. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.side_boundaries_fixed line 369
  31. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.localEdge_height_ratio line 387
  32. theorem OAI.MatchingFPRAS.Transport.IndexedCycle.cell_comparability line 415
  33. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.common_clamp_ratio line 430
  34. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.cell_clamp_comparability line 444
  35. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.drops_local line 452
  36. lemma OAI.MatchingFPRAS.Transport.IndexedCycle.additions_local line 467