OAI/Combinatorics/PortMatching/Basic.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

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

  1. abbrev OAI.Matching205.arity line 14
  2. abbrev OAI.Matching205.Vertex line 15
  3. def OAI.Matching205.port line 17
  4. def OAI.Matching205.Internal line 23
  5. def OAI.Matching205.External line 26
  6. lemma OAI.Matching205.internal_symm line 30
  7. lemma OAI.Matching205.external_symm line 33
  8. def OAI.Matching205.graph line 37
  9. lemma OAI.Matching205.port_adj line 47
  10. def OAI.Matching205.decode line 51
  11. lemma OAI.Matching205.decode_adj_iff line 62
  12. lemma OAI.Matching205.card_fiber line 66