OAI/Combinatorics/MatchingCount/Sampling/Underlying.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingFPRAS.Transport.Overlay.underlying line 14
  2. lemma OAI.MatchingFPRAS.Transport.Overlay.exists_partner line 24
  3. lemma OAI.MatchingFPRAS.Transport.Overlay.underlying_perfect line 29
  4. def OAI.MatchingFPRAS.Transport.Overlay.discrepancy line 46
  5. lemma OAI.MatchingFPRAS.Transport.Overlay.discrepancy_cycles line 49
  6. lemma OAI.MatchingFPRAS.Transport.Overlay.discrepancy_alternating line 57
  7. lemma OAI.MatchingFPRAS.Transport.Overlay.discrepancy_component_cycle line 65
  8. lemma OAI.MatchingFPRAS.Transport.Overlay.discrepancy_adj_iff line 75
  9. lemma OAI.MatchingFPRAS.Transport.Overlay.unique_colored_lift line 81
  10. lemma OAI.MatchingFPRAS.Transport.Overlay.colored_lift_mem_iff line 104
  11. lemma OAI.MatchingFPRAS.Transport.Overlay.alternating_cycle_parity line 118
  12. lemma OAI.MatchingFPRAS.Transport.Overlay.discrepancy_component_even_cycle line 154
  13. def OAI.MatchingFPRAS.Transport.Overlay.cyclicVertex line 165
  14. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicVertex_periodic line 169
  15. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicVertex_injOn line 174
  16. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicVertex_next line 184
  17. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicVertex_adj line 191
  18. def OAI.MatchingFPRAS.Transport.Overlay.cyclicEdge line 199
  19. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicEdge_spec line 205
  20. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicEdge_periodic line 214
  21. def OAI.MatchingFPRAS.Transport.Overlay.indexedCycle line 243
  22. lemma OAI.MatchingFPRAS.Transport.Overlay.indexedCycle_edge_mem line 263
  23. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicEdge_injective line 268
  24. lemma OAI.MatchingFPRAS.Transport.Overlay.alternating_edge_parity line 283
  25. lemma OAI.MatchingFPRAS.Transport.Overlay.cyclicEdge_mem_parity line 306
  26. lemma OAI.MatchingFPRAS.Transport.Overlay.parallel_component line 339
  27. theorem OAI.MatchingFPRAS.Transport.Overlay.component_classification line 380