OAI/Combinatorics/Hamiltonian/Forest.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Common-phase nonvanishing and forest extraction from actual states.

  1. structure OAI.Barnette.PermutationCoordinates line 11
  2. lemma OAI.Barnette.permutationCoordinates_exists line 17
  3. lemma OAI.Barnette.TriangleSystem.Pair.next_next_ne line 61
  4. def OAI.Barnette.TriangleSystem.Pair.cycleCoordinates line 76
  5. lemma OAI.Barnette.TriangleSystem.Pair.cycleCoordinates_faces line 79
  6. def OAI.Barnette.Network.ColoredDual.pairedCycle line 100
  7. lemma OAI.Barnette.Network.ColoredDual.pairedCycle_delta line 126
  8. lemma OAI.Barnette.Network.ColoredDual.pairedCycle_slope line 138
  9. lemma OAI.Barnette.Network.ColoredDual.paired_sign line 156
  10. lemma OAI.Barnette.Network.ColoredDual.opposite_forward_end line 166
  11. def OAI.Barnette.Network.ColoredDual.oppositeForward line 175
  12. lemma OAI.Barnette.Network.ColoredDual.oppositeForward_delta line 195
  13. lemma OAI.Barnette.Network.ColoredDual.opposite_disk line 200
  14. theorem OAI.Barnette.Network.ColoredDual.forest_pair line 234
  15. lemma OAI.Barnette.Network.connected_of_kernel_constants line 249
  16. abbrev OAI.Barnette.Network.Components line 267
  17. instance OAI.Barnette.Network.componentsFintype line 269
  18. def OAI.Barnette.Network.componentMap line 271
  19. lemma OAI.Barnette.Network.componentMap_surjective line 274
  20. lemma OAI.Barnette.Network.gradient_componentMap line 280
  21. lemma OAI.Barnette.Network.descends_components line 287