OAI/Combinatorics/HoneycombCorridor/EdgeFlow.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumBridge.Corridor.EdgeIndex line 10
  2. def OAI.PolynomialVacuumBridge.Corridor.upEnd line 12
  3. def OAI.PolynomialVacuumBridge.Corridor.downEnd line 14
  4. def OAI.PolynomialVacuumBridge.Corridor.edgeBoundary line 16
  5. theorem OAI.PolynomialVacuumBridge.Corridor.edgeBoundary_single line 19
  6. def OAI.PolynomialVacuumBridge.Corridor.edgeOf line 24
  7. def OAI.PolynomialVacuumBridge.Corridor.dartSign line 29
  8. def OAI.PolynomialVacuumBridge.Corridor.dartFlow line 33
  9. theorem OAI.PolynomialVacuumBridge.Corridor.edgeBoundary_dartFlow line 36
  10. def OAI.PolynomialVacuumBridge.Corridor.wordFlow line 43
  11. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_wordFlow line 47
  12. def OAI.PolynomialVacuumBridge.Corridor.flowComponent line 57
  13. theorem OAI.PolynomialVacuumBridge.Corridor.flowComponent_apply line 60
  14. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_up line 63
  15. theorem OAI.PolynomialVacuumBridge.Corridor.boundary_down line 74
  16. def OAI.PolynomialVacuumBridge.Corridor.closedWordFlow line 88
  17. theorem OAI.PolynomialVacuumBridge.Corridor.closed_word_has_finite_potential line 106