OAI/Combinatorics/PolynomialVacuum/Cylinder/BoundaryUniqueness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PolynomialVacuumCylinder.BoundaryArc.start_mem line 12
  2. theorem OAI.PolynomialVacuumCylinder.BoundaryArc.current_at_start line 16
  3. theorem OAI.PolynomialVacuumCylinder.BoundaryArc.ext_data line 23
  4. theorem OAI.PolynomialVacuumCylinder.not_active_zero line 31
  5. theorem OAI.PolynomialVacuumCylinder.arcs_sum_zero line 36
  6. theorem OAI.PolynomialVacuumCylinder.arcs_sum_on_member line 45
  7. theorem OAI.PolynomialVacuumCylinder.wordContour_transfer line 61
  8. theorem OAI.PolynomialVacuumCylinder.BoundaryDecomposition.on_arc line 75
  9. theorem OAI.PolynomialVacuumCylinder.BoundaryDecomposition.arc_contour line 85
  10. theorem OAI.PolynomialVacuumCylinder.BoundaryDecomposition.mem_of_contour line 91
  11. theorem OAI.PolynomialVacuumCylinder.BoundaryDecomposition.arcs_unique line 133