OAI/Combinatorics/PolynomialVacuum/Cylinder/SystemParts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumCylinder.ArcSystem.part line 9
  2. theorem OAI.PolynomialVacuumCylinder.ArcSystem.mem_part line 11
  3. theorem OAI.PolynomialVacuumCylinder.ArcSystem.part_code line 14
  4. theorem OAI.PolynomialVacuumCylinder.ArcSystem.parts_disjoint line 30
  5. theorem OAI.PolynomialVacuumCylinder.ArcSystem.parts_union line 37
  6. theorem OAI.PolynomialVacuumCylinder.ArcSystem.parts_weight line 42
  7. theorem OAI.PolynomialVacuumCylinder.ArcSystem.parts_current line 46
  8. theorem OAI.PolynomialVacuumCylinder.ArcSystem.short_top_zero line 50
  9. theorem OAI.PolynomialVacuumCylinder.ArcSystem.short_bottom_zero line 64
  10. theorem OAI.PolynomialVacuumCylinder.ArcSystem.part_length line 78
  11. theorem OAI.PolynomialVacuumCylinder.ArcSystem.parts_matches line 87