OAI/Combinatorics/PolynomialVacuum/Cylinder/Lift.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PolynomialVacuumCylinder.PlaneVertex line 8
  2. abbrev OAI.PolynomialVacuumCylinder.PlaneGerm line 9
  3. def OAI.PolynomialVacuumCylinder.projectVertex line 11
  4. def OAI.PolynomialVacuumCylinder.projectGerm line 15
  5. def OAI.PolynomialVacuumCylinder.translateVertex line 17
  6. def OAI.PolynomialVacuumCylinder.translateGerm line 21
  7. theorem OAI.PolynomialVacuumCylinder.translateVertex_zero line 23
  8. theorem OAI.PolynomialVacuumCylinder.translateGerm_zero line 24
  9. theorem OAI.PolynomialVacuumCylinder.translateVertex_add line 25
  10. theorem OAI.PolynomialVacuumCylinder.translateGerm_add line 28
  11. theorem OAI.PolynomialVacuumCylinder.translateVertex_injective line 32
  12. theorem OAI.PolynomialVacuumCylinder.translateVertex_cancel line 37
  13. theorem OAI.PolynomialVacuumCylinder.project_neighbor line 41
  14. theorem OAI.PolynomialVacuumCylinder.project_advance line 44
  15. theorem OAI.PolynomialVacuumCylinder.project_terminal line 47
  16. theorem OAI.PolynomialVacuumCylinder.project_traced line 52
  17. theorem OAI.PolynomialVacuumCylinder.translate_neighbor line 58
  18. theorem OAI.PolynomialVacuumCylinder.translate_advance line 61
  19. theorem OAI.PolynomialVacuumCylinder.translate_terminal line 64
  20. theorem OAI.PolynomialVacuumCylinder.translate_traced line 69
  21. theorem OAI.PolynomialVacuumCylinder.closure_is_translate line 75
  22. theorem OAI.PolynomialVacuumCylinder.project_translate line 96