OAI/Combinatorics/PolynomialVacuum/Cylinder/OpenNetwork.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.PolynomialVacuumCylinder.OpenNetwork line 11
  2. def OAI.PolynomialVacuumCylinder.OpenNetwork.next line 21
  3. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.next_some line 24
  4. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.next_none line 33
  5. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.next_injective line 37
  6. def OAI.PolynomialVacuumCylinder.OpenNetwork.Source line 47
  7. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.source_no_predecessor line 49
  8. def OAI.PolynomialVacuumCylinder.OpenNetwork.pathLength line 57
  9. def OAI.PolynomialVacuumCylinder.OpenNetwork.pathSite line 59
  10. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.pathLength_pos line 62
  11. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.pathSite_injective line 65
  12. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.pathSite_start line 68
  13. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.pathSite_next line 72
  14. theorem OAI.PolynomialVacuumCylinder.OpenNetwork.pathSite_exit line 77