OAI/Combinatorics/PortMatching/Decoding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

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

  1. lemma OAI.Matching205.Reverse.unique_missing line 13
  2. def OAI.Matching205.Reverse.mate line 28
  3. lemma OAI.Matching205.Reverse.mate_adj line 30
  4. lemma OAI.Matching205.Reverse.mate_eq line 33
  5. lemma OAI.Matching205.Reverse.mate_involutive line 36
  6. def OAI.Matching205.Reverse.evenPosition line 40
  7. def OAI.Matching205.Reverse.nonport line 42
  8. lemma OAI.Matching205.Reverse.evenPosition_injective line 44
  9. lemma OAI.Matching205.Reverse.nonport_injective line 51
  10. lemma OAI.Matching205.Reverse.port_eq_evenPosition line 57
  11. lemma OAI.Matching205.Reverse.nonport_not_external line 61
  12. lemma OAI.Matching205.Reverse.internal_nonport_even line 68
  13. lemma OAI.Matching205.Reverse.internal_even_nonport line 86
  14. lemma OAI.Matching205.Reverse.mate_nonport_even line 104
  15. def OAI.Matching205.Reverse.pairedPort line 114
  16. lemma OAI.Matching205.Reverse.pairedPort_spec line 118
  17. lemma OAI.Matching205.Reverse.pairedPort_injective line 123
  18. lemma OAI.Matching205.Reverse.external_iff_missing line 131
  19. theorem OAI.Matching205.Reverse.unique_external_port line 155
  20. theorem OAI.Matching205.decode_isPerfectMatching line 168