OAI/Combinatorics/Hamiltonian/BMatching.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Integral flows, capacitated matchings, and incidence-state pairs.

  1. lemma OAI.Barnette.BMatching.count_sum line 12
  2. lemma OAI.Barnette.BMatching.count_prod line 17
  3. abbrev OAI.Barnette.BMatching.Inc line 21
  4. abbrev OAI.Barnette.BMatching.Left line 22
  5. abbrev OAI.Barnette.BMatching.Right line 23
  6. def OAI.Barnette.BMatching.gadget line 25
  7. lemma OAI.Barnette.BMatching.incidence_fiber line 31
  8. lemma OAI.Barnette.BMatching.gadget_hall line 45
  9. theorem OAI.Barnette.BMatching.gadget_matching line 138
  10. structure OAI.Barnette.BMatching.FactorData line 154
  11. lemma OAI.Barnette.BMatching.data_of_gadget line 162
  12. lemma OAI.Barnette.BMatching.two_image_count line 211
  13. lemma OAI.Barnette.BMatching.data_two_factor line 217
  14. lemma OAI.Barnette.BMatching.regular_hall line 254
  15. lemma OAI.Barnette.BMatching.regular_matching line 277
  16. theorem OAI.Barnette.BMatching.two_matchings line 286
  17. lemma OAI.Barnette.TriangleSystem.State.exists_value line 319
  18. lemma OAI.Barnette.Network.ColoredDual.nonroots_card line 341
  19. lemma OAI.Barnette.Network.ColoredDual.corner_filter_card line 361
  20. lemma OAI.Barnette.Network.ColoredDual.state_capacity line 378
  21. theorem OAI.Barnette.Network.ColoredDual.pair_nonempty line 403