OAI/Geometry/NearbyLagrangian/StableFibers.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

Stable fiber families and the negative spherical class.

  1. structure OAI.NearbyLagrangian.FiberFamily line 15
  2. def OAI.NearbyLagrangian.FiberFamily.ofProjection line 25
  3. def OAI.NearbyLagrangian.FiberFamily.suspend line 28
  4. def OAI.NearbyLagrangian.FiberFamily.iterate line 31
  5. lemma OAI.NearbyLagrangian.FiberFamily.iterate_zero line 35
  6. lemma OAI.NearbyLagrangian.FiberFamily.iterate_succ line 36
  7. lemma OAI.NearbyLagrangian.FiberFamily.iterate_add line 39
  8. lemma OAI.NearbyLagrangian.FiberFamily.suspend_iterate line 45
  9. def OAI.NearbyLagrangian.FiberFamily.Equiv line 51
  10. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.refl line 55
  11. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.symm line 56
  12. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.trans line 59
  13. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.suspend line 65
  14. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.iterate line 69
  15. def OAI.NearbyLagrangian.FiberFamily.StableEquiv line 76
  16. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.refl line 80
  17. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.symm line 81
  18. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.trans line 85
  19. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.suspend line 96
  20. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.of_suspend line 103
  21. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.suspend_iff line 109
  22. theorem OAI.NearbyLagrangian.FiberFamily.StableEquiv.iterate_iff line 112
  23. theorem OAI.NearbyLagrangian.FiberFamily.Equiv.stable line 119
  24. lemma OAI.NearbyLagrangian.RadialTopology.isCompact_negativeSphere line 137
  25. lemma OAI.NearbyLagrangian.RadialTopology.isCompact_fullSphere line 146
  26. def OAI.NearbyLagrangian.RadialTopology.sphereFiberFamily line 155
  27. def OAI.NearbyLagrangian.RadialTopology.suspendedSphereFiberFamily line 158
  28. lemma OAI.NearbyLagrangian.RadialTopology.sphereFiberFamily_suspend line 161
  29. def OAI.NearbyLagrangian.Tubes.angularFamily line 171
  30. def OAI.NearbyLagrangian.Tubes.roundFamily line 174
  31. lemma OAI.NearbyLagrangian.Tubes.angularFamily_addPositive line 177
  32. lemma OAI.NearbyLagrangian.Tubes.roundFamily_succ line 193
  33. lemma OAI.NearbyLagrangian.Tubes.roundFamily_iterate line 203
  34. lemma OAI.NearbyLagrangian.Tubes.angularFamily_addNegative line 213
  35. theorem OAI.NearbyLagrangian.Tubes.angularFamily_stabilize line 241
  36. theorem OAI.NearbyLagrangian.Tubes.angularFamily_stabilizeFor line 250
  37. theorem OAI.NearbyLagrangian.Tubes.StableNegativeTrivial.finite_spherical line 261
  38. abbrev OAI.NearbyLagrangian.FiberFamily.Graded line 284
  39. def OAI.NearbyLagrangian.FiberFamily.Graded.Rel line 286
  40. theorem OAI.NearbyLagrangian.FiberFamily.Graded.Rel.refl line 290
  41. theorem OAI.NearbyLagrangian.FiberFamily.Graded.Rel.symm line 291
  42. theorem OAI.NearbyLagrangian.FiberFamily.Graded.Rel.trans line 292
  43. def OAI.NearbyLagrangian.FiberFamily.gradedSetoid line 302
  44. abbrev OAI.NearbyLagrangian.FiberFamily.StableClass line 306
  45. def OAI.NearbyLagrangian.FiberFamily.classOf line 308
  46. theorem OAI.NearbyLagrangian.FiberFamily.classOf_eq_iff line 310
  47. theorem OAI.NearbyLagrangian.FiberFamily.classOf_sameGrade line 313
  48. theorem OAI.NearbyLagrangian.FiberFamily.classOf_suspend line 317
  49. theorem OAI.NearbyLagrangian.FiberFamily.classOf_equiv line 321
  50. theorem OAI.NearbyLagrangian.Tubes.stableNegativeTrivial_iff_finite_spherical line 332
  51. def OAI.NearbyLagrangian.Tubes.standardSphericalClass line 341
  52. theorem OAI.NearbyLagrangian.Tubes.round_family_class line 344
  53. def OAI.NearbyLagrangian.Tubes.negativeStableClass line 350
  54. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_eq line 354
  55. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_stabilize line 360
  56. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_stabilizeFor line 365
  57. theorem OAI.NearbyLagrangian.Tubes.angularFamily_homotopic line 373
  58. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_homotopic line 383
  59. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_eq_standard_iff line 390