OAI/Combinatorics/PolynomialVacuum/Cylinder/NetworkCycles.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PolynomialVacuumCylinder.ClosedNetwork line 11
  2. def OAI.PolynomialVacuumCylinder.ClosedNetwork.germ line 23
  3. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.exists_turn line 25
  4. def OAI.PolynomialVacuumCylinder.ClosedNetwork.turn line 30
  5. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.outgoing_turn line 32
  6. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.advance_turn line 35
  7. def OAI.PolynomialVacuumCylinder.ClosedNetwork.word line 40
  8. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.word_length line 44
  9. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.terminal_word line 47
  10. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.traced_word line 53
  11. def OAI.PolynomialVacuumCylinder.ClosedNetwork.period line 62
  12. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.period_pos line 64
  13. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.orbit_terminal line 67
  14. theorem OAI.PolynomialVacuumCylinder.ClosedNetwork.orbit_nodup line 72
  15. def OAI.PolynomialVacuumCylinder.ClosedNetwork.polygon line 80