OAI/Combinatorics/Hamiltonian/ForestMatching.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

From opposite forests to connected spanning matching complements.

  1. lemma OAI.Barnette.Network.complement_coloring line 13
  2. lemma OAI.Barnette.Network.colored_endpoints line 18
  3. lemma OAI.Barnette.Network.black_fiber_count line 25
  4. lemma OAI.Barnette.Network.tree_matching line 51
  5. lemma OAI.Barnette.Network.sum_substars line 157
  6. lemma OAI.Barnette.Network.matching_cut_balance line 176
  7. lemma OAI.Barnette.Network.ColoredDual.black_white_balance line 219
  8. lemma OAI.Barnette.Network.ColoredDual.recovery_matching line 226
  9. abbrev OAI.Barnette.CycleCoordinates.reverseCycle line 236
  10. lemma OAI.Barnette.Network.directed_cycle_of_not_acyclic line 249
  11. def OAI.Barnette.Network.matchingEdge line 279
  12. lemma OAI.Barnette.Network.matchingEdge_spec line 282
  13. lemma OAI.Barnette.Network.matchingEdge_mem line 286
  14. lemma OAI.Barnette.Network.matchingEdge_eq line 290
  15. abbrev OAI.Barnette.Network.ColoredDual.selectNet line 302
  16. lemma OAI.Barnette.Network.ColoredDual.selectNet_forest line 307
  17. lemma OAI.Barnette.Network.ColoredDual.selected_forest line 338
  18. lemma OAI.Barnette.Network.ColoredDual.recover_connected_complement line 375