OAI/Combinatorics/PolynomialVacuum/Cylinder/ArcIsometries.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PolynomialVacuumCylinder.translate line 9
  2. def OAI.PolynomialVacuumCylinder.rotate line 12
  3. def OAI.PolynomialVacuumCylinder.mapGerm line 15
  4. theorem OAI.PolynomialVacuumCylinder.translate_neighbor_cyl line 17
  5. theorem OAI.PolynomialVacuumCylinder.rotate_neighbor line 20
  6. theorem OAI.PolynomialVacuumCylinder.rotate_invol line 23
  7. theorem OAI.PolynomialVacuumCylinder.translate_comp line 25
  8. theorem OAI.PolynomialVacuumCylinder.translate_zero line 28
  9. theorem OAI.PolynomialVacuumCylinder.translate_injective line 30
  10. theorem OAI.PolynomialVacuumCylinder.map_advance line 35
  11. theorem OAI.PolynomialVacuumCylinder.map_terminal line 38
  12. theorem OAI.PolynomialVacuumCylinder.map_traced line 43
  13. theorem OAI.PolynomialVacuumCylinder.translate_layer line 48
  14. theorem OAI.PolynomialVacuumCylinder.rotate_layer line 50
  15. theorem OAI.PolynomialVacuumCylinder.rotate_band line 53
  16. theorem OAI.PolynomialVacuumCylinder.translate_band line 57