OAI/Combinatorics/HoneycombCorridor/Contours.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumBridge.Corridor.orientedFlow line 11
  2. theorem OAI.PolynomialVacuumBridge.Corridor.orientedFlow_single line 15
  3. theorem OAI.PolynomialVacuumBridge.Corridor.orientedFlow_dartFlow line 20
  4. def OAI.PolynomialVacuumBridge.Corridor.turnVisit line 26
  5. theorem OAI.PolynomialVacuumBridge.Corridor.orientedFlow_wordFlow line 32
  6. theorem OAI.PolynomialVacuumBridge.Corridor.turnVisit_eq_zero_of_not_mem line 43
  7. theorem OAI.PolynomialVacuumBridge.Corridor.simple_closed_word_local line 55
  8. theorem OAI.PolynomialVacuumBridge.Corridor.orientedFlow_up line 67
  9. theorem OAI.PolynomialVacuumBridge.Corridor.orientedFlow_down line 78
  10. def OAI.PolynomialVacuumBridge.Corridor.leftFace line 91
  11. def OAI.PolynomialVacuumBridge.Corridor.rightFace line 95
  12. def OAI.PolynomialVacuumBridge.Corridor.RepresentsFlow line 97
  13. theorem OAI.PolynomialVacuumBridge.Corridor.closed_word_has_potential line 100
  14. theorem OAI.PolynomialVacuumBridge.Corridor.wordFlow_append line 121
  15. theorem OAI.PolynomialVacuumBridge.Corridor.closed_word_rotate line 127
  16. def OAI.PolynomialVacuumBridge.Corridor.LocalContour line 138
  17. def OAI.PolynomialVacuumBridge.Corridor.WordContour line 142
  18. theorem OAI.PolynomialVacuumBridge.Corridor.wordContour_of_splits line 146
  19. theorem OAI.PolynomialVacuumBridge.Corridor.simple_closed_word_contour line 156
  20. theorem OAI.PolynomialVacuumBridge.Corridor.localContour_sides line 167
  21. theorem OAI.PolynomialVacuumBridge.Corridor.wordContour_sides line 179
  22. theorem OAI.PolynomialVacuumBridge.Corridor.rightFace_reverse line 192
  23. theorem OAI.PolynomialVacuumBridge.Corridor.reverseGerm_advance line 195
  24. def OAI.PolynomialVacuumBridge.Corridor.canonicalDart line 199
  25. theorem OAI.PolynomialVacuumBridge.Corridor.canonicalDart_edgeOf line 201
  26. def OAI.PolynomialVacuumBridge.Corridor.SideValues line 207
  27. theorem OAI.PolynomialVacuumBridge.Corridor.SideValues.reverse line 211
  28. theorem OAI.PolynomialVacuumBridge.Corridor.SideValues.canonical line 215
  29. theorem OAI.PolynomialVacuumBridge.Corridor.wordFlow_edge_sides line 221
  30. theorem OAI.PolynomialVacuumBridge.Corridor.RepresentsFlow.horizontal line 244
  31. theorem OAI.PolynomialVacuumBridge.Corridor.finite_potential_has_zero_side line 251
  32. theorem OAI.PolynomialVacuumBridge.Corridor.finite_potential_two_values line 264
  33. theorem OAI.PolynomialVacuumBridge.Corridor.simple_closed_word_indicator line 295