OAI/GroupTheory/UniversalGroup/Cylinders.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniversalFInfinity.Cylinder.Disk line 20
  2. abbrev OAI.UniversalFInfinity.Cylinder.Sphere line 21
  3. abbrev OAI.UniversalFInfinity.Cylinder.Rim line 22
  4. def OAI.UniversalFInfinity.Cylinder.denominator line 25
  5. lemma OAI.UniversalFInfinity.Cylinder.denominator_bounds line 26
  6. lemma OAI.UniversalFInfinity.Cylinder.denominator_pos line 33
  7. def OAI.UniversalFInfinity.Cylinder.factor line 36
  8. lemma OAI.UniversalFInfinity.Cylinder.factor_mul_denominator line 37
  9. lemma OAI.UniversalFInfinity.Cylinder.factor_bounds line 39
  10. lemma OAI.UniversalFInfinity.Cylinder.factor_nonneg line 44
  11. lemma OAI.UniversalFInfinity.Cylinder.retract_time_mem line 46
  12. lemma OAI.UniversalFInfinity.Cylinder.retract_disk_mem line 57
  13. lemma OAI.UniversalFInfinity.Cylinder.retract_mem_rim line 65
  14. lemma OAI.UniversalFInfinity.Cylinder.continuous_denominator line 82
  15. lemma OAI.UniversalFInfinity.Cylinder.continuous_factor line 85
  16. def OAI.UniversalFInfinity.Cylinder.retract line 88
  17. lemma OAI.UniversalFInfinity.Cylinder.retract_of_rim line 99
  18. lemma OAI.UniversalFInfinity.Cylinder.continuous_finite_closed_paste line 123
  19. def OAI.UniversalFInfinity.Cylinder.face line 133
  20. lemma OAI.UniversalFInfinity.Cylinder.face_closed line 136
  21. lemma OAI.UniversalFInfinity.Cylinder.face_cover line 140
  22. def OAI.UniversalFInfinity.Cylinder.faceValue line 147
  23. lemma OAI.UniversalFInfinity.Cylinder.faceValue_compatible line 156
  24. def OAI.UniversalFInfinity.Cylinder.rimMap line 167
  25. lemma OAI.UniversalFInfinity.Cylinder.rimMap_face line 170
  26. def OAI.UniversalFInfinity.Cylinder.extension line 174
  27. lemma OAI.UniversalFInfinity.Cylinder.extension_zero line 176
  28. lemma OAI.UniversalFInfinity.Cylinder.extension_boundary line 183
  29. theorem OAI.UniversalFInfinity.Cylinder.homotopy_extension line 193
  30. def OAI.UniversalFInfinity.SphereCube.rimSphere line 206
  31. def OAI.UniversalFInfinity.SphereCube.rimSide line 215
  32. def OAI.UniversalFInfinity.SphereCube.rimBottom line 219
  33. def OAI.UniversalFInfinity.SphereCube.top line 222
  34. lemma OAI.UniversalFInfinity.SphereCube.rim_contractible line 227
  35. lemma OAI.UniversalFInfinity.SphereCube.rim_nullhomotopy line 242
  36. def OAI.UniversalFInfinity.SphereCube.edgeTrace line 259
  37. lemma OAI.UniversalFInfinity.SphereCube.edgeTrace_zero line 264
  38. def OAI.UniversalFInfinity.SphereCube.topExtension line 269
  39. lemma OAI.UniversalFInfinity.SphereCube.topExtension_zero line 272
  40. lemma OAI.UniversalFInfinity.SphereCube.topExtension_boundary line 274
  41. def OAI.UniversalFInfinity.SphereCube.normalizedTop line 278
  42. lemma OAI.UniversalFInfinity.SphereCube.normalizedTop_boundary line 280
  43. def OAI.UniversalFInfinity.SphereCube.sidePaths line 284
  44. def OAI.UniversalFInfinity.SphereCube.bottomPaths line 289
  45. def OAI.UniversalFInfinity.SphereCube.topPaths line 294
  46. lemma OAI.UniversalFInfinity.SphereCube.spherePaths_compatible line 297
  47. lemma OAI.UniversalFInfinity.SphereCube.spherePaths_compatible_map line 306
  48. def OAI.UniversalFInfinity.SphereCube.spherePaths line 311
  49. lemma OAI.UniversalFInfinity.SphereCube.cons_tail_time line 315
  50. lemma OAI.UniversalFInfinity.SphereCube.spherePaths_zero line 322
  51. def OAI.UniversalFInfinity.SphereCube.normalizedSphere line 350
  52. def OAI.UniversalFInfinity.SphereCube.normalizeHomotopy line 353
  53. lemma OAI.UniversalFInfinity.SphereCube.normalizedSphere_rim line 359
  54. lemma OAI.UniversalFInfinity.SphereCube.normalizedSphere_top line 374
  55. abbrev OAI.UniversalFInfinity.DiskCube.Disk line 386
  56. abbrev OAI.UniversalFInfinity.DiskCube.Sphere line 387
  57. def OAI.UniversalFInfinity.DiskCube.toCube line 389
  58. def OAI.UniversalFInfinity.DiskCube.fromCube line 398
  59. lemma OAI.UniversalFInfinity.DiskCube.from_to line 410
  60. lemma OAI.UniversalFInfinity.DiskCube.to_from line 416
  61. lemma OAI.UniversalFInfinity.DiskCube.from_boundary line 422
  62. lemma OAI.UniversalFInfinity.DiskCube.to_boundary line 434