OAI/Combinatorics/PortMatching/Extension.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Perfect-matching-preserving port-path degree reduction for finite simple graphs.

  1. def OAI.Matching205.Forward.Pair line 11
  2. lemma OAI.Matching205.Forward.pair_symm line 17
  3. lemma OAI.Matching205.Forward.pair_consecutive line 24
  4. lemma OAI.Matching205.Forward.pair_not_center line 29
  5. lemma OAI.Matching205.Forward.pair_completion line 33
  6. lemma OAI.Matching205.Forward.unique_neighbor line 58
  7. def OAI.Matching205.Forward.neighbor line 61
  8. lemma OAI.Matching205.Forward.neighbor_adj line 66
  9. def OAI.Matching205.Forward.center line 69
  10. def OAI.Matching205.Forward.selected line 72
  11. lemma OAI.Matching205.Forward.port_eq_selected line 74
  12. def OAI.Matching205.Forward.Local line 82
  13. def OAI.Matching205.Forward.Across line 85
  14. lemma OAI.Matching205.Forward.local_symm line 88
  15. lemma OAI.Matching205.Forward.across_symm line 97
  16. lemma OAI.Matching205.Forward.across_selected line 100
  17. lemma OAI.Matching205.Forward.across_unique line 106
  18. lemma OAI.Matching205.Forward.selected_across line 114
  19. lemma OAI.Matching205.Forward.local_not_selected line 120
  20. lemma OAI.Matching205.Forward.local_completion line 128
  21. def OAI.Matching205.Forward.extend line 147
  22. theorem OAI.Matching205.Forward.extend_perfect line 161
  23. theorem OAI.Matching205.Forward.decode_extend_adj line 180