OAI/Combinatorics/PolynomialVacuum/Cylinder/FiniteArcs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumCylinder.BoundaryArc.length_le line 11
  2. def OAI.PolynomialVacuumCylinder.BoundaryArc.finiteCode line 16
  3. theorem OAI.PolynomialVacuumCylinder.BoundaryArc.finiteCode_injective line 19
  4. instance OAI.PolynomialVacuumCylinder.boundaryArc_finite line 25
  5. instance OAI.PolynomialVacuumCylinder.(instance at line 26) line 26
  6. abbrev OAI.PolynomialVacuumCylinder.ArcSystem line 28
  7. def OAI.PolynomialVacuumCylinder.ArcSystem.vertices line 30
  8. def OAI.PolynomialVacuumCylinder.ArcSystem.current line 31
  9. def OAI.PolynomialVacuumCylinder.ArcSystem.weight line 32