OAI/Combinatorics/PortMatching/Size.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

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

  1. instance OAI.Matching205.graphAdjDecidable line 14
  2. lemma OAI.Matching205.size_vertex_ext line 17
  3. lemma OAI.Matching205.size_port_injective line 26
  4. lemma OAI.Matching205.size_external_base_ne line 35
  5. lemma OAI.Matching205.size_external_unique line 40
  6. def OAI.Matching205.size_neighborCode line 53
  7. lemma OAI.Matching205.size_neighborCode_injective line 59
  8. theorem OAI.Matching205.graph_degree_le_three line 83
  9. theorem OAI.Matching205.card_vertex_add_card line 89
  10. theorem OAI.Matching205.card_vertex line 107