OAI/Combinatorics/Hamiltonian/Matching.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Disk and spoke signs and matching complements.

  1. lemma OAI.Barnette.CycleCoordinates.not_acyclic line 10
  2. lemma OAI.Barnette.Network.acyclic_conserved_zero line 27
  3. lemma OAI.Barnette.Network.Simple.restrict line 55
  4. lemma OAI.Barnette.Network.extend_restriction line 61
  5. lemma OAI.Barnette.Network.conserved_supported_acyclic line 68
  6. lemma OAI.Barnette.Network.Duality.complement_connected line 79
  7. def OAI.Barnette.Network.addSink line 101
  8. lemma OAI.Barnette.Network.addSink_tail_injective line 105
  9. lemma OAI.Barnette.Network.addSink_acyclic line 114
  10. lemma OAI.Barnette.Network.boundary_injective_of_tree_card line 158
  11. lemma OAI.Barnette.Network.boundary_restrict_injective line 164
  12. lemma OAI.Barnette.Network.boundary_supported_vertices line 173
  13. lemma OAI.Barnette.Network.independent_edges_bound line 183
  14. abbrev OAI.Barnette.Network.ColoredDual.QNet line 225
  15. lemma OAI.Barnette.Network.ColoredDual.pair_val_ne line 230
  16. lemma OAI.Barnette.Network.ColoredDual.q_graph line 234
  17. def OAI.Barnette.Network.ColoredDual.qLabel line 249
  18. lemma OAI.Barnette.Network.ColoredDual.qLabel_ends line 253
  19. lemma OAI.Barnette.Network.ColoredDual.qLabel_black line 259
  20. lemma OAI.Barnette.Network.ColoredDual.qLabel_inj line 265
  21. def OAI.Barnette.Network.ColoredDual.rootStart line 271
  22. lemma OAI.Barnette.Network.ColoredDual.rootStart_inj line 273
  23. lemma OAI.Barnette.Network.ColoredDual.rootStart_ne line 274
  24. abbrev OAI.Barnette.Network.ColoredDual.augQ line 276
  25. lemma OAI.Barnette.Network.ColoredDual.augQ_acyclic line 281
  26. def OAI.Barnette.Network.ColoredDual.augLabel line 292
  27. lemma OAI.Barnette.Network.ColoredDual.augLabel_ends line 297
  28. lemma OAI.Barnette.Network.ColoredDual.augLabel_inj line 306
  29. def OAI.Barnette.Network.ColoredDual.removed line 326
  30. lemma OAI.Barnette.Network.ColoredDual.removed_acyclic line 330
  31. lemma OAI.Barnette.Network.ColoredDual.remainder_connected line 342
  32. lemma OAI.Barnette.Network.ColoredDual.removed_card line 348
  33. lemma OAI.Barnette.Network.Triangle.edge_incident line 365
  34. lemma OAI.Barnette.Network.Triangle.other_root_sides line 370
  35. lemma OAI.Barnette.Network.Triangle.opposite_characteristic line 383
  36. lemma OAI.Barnette.Network.ColoredDual.removed_at_black line 409
  37. lemma OAI.Barnette.Network.ColoredDual.remainder_black_degree line 444
  38. lemma OAI.Barnette.Network.ColoredDual.cubic_cards line 477
  39. lemma OAI.Barnette.Network.ColoredDual.remainder_independent line 487
  40. lemma OAI.Barnette.Network.ColoredDual.remainder_incident line 499