OAI/Combinatorics/Hamiltonian/MinorDuality.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact duality under finite network minors.

  1. def OAI.Barnette.Network.fullBlack line 13
  2. def OAI.Barnette.Network.regionBlack line 16
  3. lemma OAI.Barnette.Network.sum_regionBlack line 20
  4. lemma OAI.Barnette.Network.regionBalance_singleton line 27
  5. lemma OAI.Barnette.Network.regionBalance_complement_singleton line 33
  6. lemma OAI.Barnette.Network.singleton_regionBlack line 43
  7. lemma OAI.Barnette.Network.region_density line 55
  8. theorem OAI.Barnette.Network.induced_density line 87
  9. lemma OAI.Barnette.Network.three_corner_count line 115
  10. lemma OAI.Barnette.Network.Triangle.edges_in_count line 126
  11. lemma OAI.Barnette.Network.Triangle.all_corners line 141
  12. lemma OAI.Barnette.Network.black_edge_partition line 159
  13. lemma OAI.Barnette.Network.black_dual_card line 179
  14. lemma OAI.Barnette.Network.capacity_identity line 195
  15. theorem OAI.Barnette.Network.capacity_full line 220