OAI/Topology/Homotopy/FiberCone.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

Fiberwise cones, contractions and left suspension homotopies.

  1. abbrev OAI.NearbyLagrangian.FiberCone.Raw line 17
  2. inductive OAI.NearbyLagrangian.FiberCone.Seam line 19
  3. def OAI.NearbyLagrangian.FiberCone.Space line 23
  4. instance OAI.NearbyLagrangian.FiberCone.(instance at line 24) line 24
  5. def OAI.NearbyLagrangian.FiberCone.base line 27
  6. def OAI.NearbyLagrangian.FiberCone.ray line 29
  7. def OAI.NearbyLagrangian.FiberCone.apex line 32
  8. lemma OAI.NearbyLagrangian.FiberCone.ray_zero line 36
  9. lemma OAI.NearbyLagrangian.FiberCone.ray_one line 38
  10. def OAI.NearbyLagrangian.FiberCone.lift line 41
  11. lemma OAI.NearbyLagrangian.FiberCone.lift_base line 53
  12. lemma OAI.NearbyLagrangian.FiberCone.lift_ray line 57
  13. lemma OAI.NearbyLagrangian.FiberCone.lift_apex line 61
  14. theorem OAI.NearbyLagrangian.FiberCone.induction line 66
  15. def OAI.NearbyLagrangian.FiberCone.projection line 76
  16. lemma OAI.NearbyLagrangian.FiberCone.projection_base line 81
  17. lemma OAI.NearbyLagrangian.FiberCone.projection_ray line 83
  18. lemma OAI.NearbyLagrangian.FiberCone.projection_apex line 86
  19. abbrev OAI.NearbyLagrangian.FiberCone.Susp line 89
  20. def OAI.NearbyLagrangian.FiberCone.suspProjection line 91
  21. abbrev OAI.NearbyLagrangian.FiberCone.south line 94
  22. abbrev OAI.NearbyLagrangian.FiberCone.meridian line 95
  23. abbrev OAI.NearbyLagrangian.FiberCone.north line 96
  24. def OAI.NearbyLagrangian.FiberCone.suspMap line 98
  25. lemma OAI.NearbyLagrangian.FiberCone.suspMap_south line 106
  26. lemma OAI.NearbyLagrangian.FiberCone.suspMap_meridian line 108
  27. lemma OAI.NearbyLagrangian.FiberCone.suspMap_north line 111
  28. lemma OAI.NearbyLagrangian.FiberCone.suspMap_over line 114
  29. def OAI.NearbyLagrangian.FiberCone.collapse line 122
  30. lemma OAI.NearbyLagrangian.FiberCone.collapse_base line 128
  31. lemma OAI.NearbyLagrangian.FiberCone.collapse_ray line 130
  32. lemma OAI.NearbyLagrangian.FiberCone.collapse_apex line 132
  33. lemma OAI.NearbyLagrangian.FiberCone.collapse_over line 135
  34. structure OAI.NearbyLagrangian.FiberCone.Contraction line 155
  35. def OAI.NearbyLagrangian.FiberCone.Contraction.inverseRay line 167
  36. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverseRay_zero line 172
  37. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverseRay_one line 175
  38. def OAI.NearbyLagrangian.FiberCone.Contraction.inverse line 179
  39. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverse_south line 182
  40. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverse_meridian line 183
  41. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverse_north line 185
  42. lemma OAI.NearbyLagrangian.FiberCone.Contraction.inverse_over line 187
  43. def OAI.NearbyLagrangian.FiberCone.squareDen line 197
  44. lemma OAI.NearbyLagrangian.FiberCone.squareDen_pos line 198
  45. lemma OAI.NearbyLagrangian.FiberCone.continuous_squareDen line 203
  46. def OAI.NearbyLagrangian.FiberCone.horizontal line 206
  47. def OAI.NearbyLagrangian.FiberCone.vertical line 221
  48. lemma OAI.NearbyLagrangian.FiberCone.horizontal_left line 235
  49. lemma OAI.NearbyLagrangian.FiberCone.horizontal_right line 238
  50. lemma OAI.NearbyLagrangian.FiberCone.vertical_left line 241
  51. lemma OAI.NearbyLagrangian.FiberCone.vertical_right line 244
  52. lemma OAI.NearbyLagrangian.FiberCone.horizontal_bottom line 247
  53. lemma OAI.NearbyLagrangian.FiberCone.vertical_bottom line 250
  54. lemma OAI.NearbyLagrangian.FiberCone.square_top line 254
  55. def OAI.NearbyLagrangian.FiberCone.cylinderLift line 284
  56. lemma OAI.NearbyLagrangian.FiberCone.cylinderLift_base line 295
  57. lemma OAI.NearbyLagrangian.FiberCone.cylinderLift_ray line 300
  58. lemma OAI.NearbyLagrangian.FiberCone.cylinderLift_apex line 305
  59. def OAI.NearbyLagrangian.FiberCone.Contraction.leftRay line 315
  60. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftRay_bottom line 324
  61. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftRay_top line 328
  62. def OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation line 334
  63. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_south line 338
  64. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_meridian line 340
  65. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_north line 342
  66. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_zero line 345
  67. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_one line 355
  68. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftDeformation_over line 366
  69. def OAI.NearbyLagrangian.FiberCone.Contraction.leftHomotopy line 378
  70. lemma OAI.NearbyLagrangian.FiberCone.Contraction.leftHomotopy_over line 384