OAI/Geometry/NearbyLagrangian/TubeClasses.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Directed tube classes and their stable negative fiber classes.

  1. def OAI.NearbyLagrangian.Tubes.stabilizeTo line 15
  2. theorem OAI.NearbyLagrangian.Tubes.stabilizeTo_self line 19
  3. theorem OAI.NearbyLagrangian.Tubes.stabilizeTo_succ line 22
  4. theorem OAI.NearbyLagrangian.Tubes.stabilizeTo_add line 26
  5. theorem OAI.NearbyLagrangian.Tubes.stabilizeTo_comp line 35
  6. theorem OAI.NearbyLagrangian.Tubes.stabilizeTo_standard line 43
  7. def OAI.NearbyLagrangian.Tubes.tubeHomotopySetoid line 50
  8. abbrev OAI.NearbyLagrangian.Tubes.TubeHomotopyClass line 54
  9. structure OAI.NearbyLagrangian.Tubes.TubeClassMap line 56
  10. instance OAI.NearbyLagrangian.Tubes.(instance at line 59) line 59
  11. def OAI.NearbyLagrangian.Tubes.stabilizeClass line 64
  12. instance OAI.NearbyLagrangian.Tubes.(instance at line 69) line 69
  13. abbrev OAI.NearbyLagrangian.Tubes.StableTubeClass line 87
  14. def OAI.NearbyLagrangian.Tubes.stableClass line 89
  15. def OAI.NearbyLagrangian.Tubes.standardStableClass line 92
  16. theorem OAI.NearbyLagrangian.Tubes.stableClass_stabilizeTo line 95
  17. theorem OAI.NearbyLagrangian.Tubes.stableClass_standard line 104
  18. theorem OAI.NearbyLagrangian.Tubes.stableClass_eq_iff line 110
  19. instance OAI.NearbyLagrangian.Tubes.tubePathConnected line 122

    Distinct definitions of this name: OAI/Geometry/NearbyLagrangian/SphereCollapse.lean:215 (same statement text; different proof or body). Qualify references as OAI.NearbyLagrangian.Tubes.tubePathConnected@path.

  20. theorem OAI.NearbyLagrangian.Tubes.nullhomotopic_iff_standard line 125
  21. theorem OAI.NearbyLagrangian.Tubes.stablyNonNull_iff_class_ne line 134
  22. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_stabilizeTo line 165
  23. def OAI.NearbyLagrangian.Tubes.negativeClassOnStage line 171
  24. theorem OAI.NearbyLagrangian.Tubes.negativeClassOnStage_compatible line 176
  25. def OAI.NearbyLagrangian.Tubes.stableNegativeClass line 182
  26. theorem OAI.NearbyLagrangian.Tubes.stableNegativeClass_apply line 193
  27. theorem OAI.NearbyLagrangian.Tubes.negativeStableClass_standard line 196
  28. theorem OAI.NearbyLagrangian.Tubes.stableNegativeClass_standard line 207
  29. theorem OAI.NearbyLagrangian.Tubes.stableClass_rep_above line 213
  30. theorem OAI.NearbyLagrangian.Tubes.exists_kernel_family_iff line 227
  31. theorem OAI.NearbyLagrangian.Tubes.kernelFamilyGoal_iff_actual_nontrivial_fiber line 242