OAI/Topology/Homotopy/CubicalSpheres.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Cubical and spherical representatives of homotopy classes.

  1. def OAI.NearbyLagrangian.CubicalSphere.interiorCube line 17
  2. lemma OAI.NearbyLagrangian.CubicalSphere.interiorCube_eq line 19
  3. lemma OAI.NearbyLagrangian.CubicalSphere.isOpen_interiorCube line 33
  4. lemma OAI.NearbyLagrangian.CubicalSphere.complement_nonempty line 42
  5. def OAI.NearbyLagrangian.CubicalSphere.interiorHomeomorph line 47
  6. def OAI.NearbyLagrangian.CubicalSphere.intervalHomeomorph line 63
  7. def OAI.NearbyLagrangian.CubicalSphere.interiorEuclidean line 75
  8. def OAI.NearbyLagrangian.CubicalSphere.compactificationSphere line 79
  9. def OAI.NearbyLagrangian.CubicalSphere.spherePoint line 84
  10. def OAI.NearbyLagrangian.CubicalSphere.sphereQuotient line 87
  11. lemma OAI.NearbyLagrangian.CubicalSphere.sphereQuotient_boundary line 93
  12. lemma OAI.NearbyLagrangian.CubicalSphere.sphereQuotient_surjective line 99
  13. def OAI.NearbyLagrangian.CubicalSphere.sphereMap line 105
  14. lemma OAI.NearbyLagrangian.CubicalSphere.sphereMap_quotient line 111
  15. lemma OAI.NearbyLagrangian.CubicalSphere.sphereMap_point line 117
  16. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_null_implies_cube_null line 123
  17. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_null_implies_class_one line 138
  18. def OAI.NearbyLagrangian.CubicalSphere.sphereHomotopy line 156
  19. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_const line 187
  20. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_null_iff_cube_null line 193
  21. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_null_iff_class_one line 202
  22. def OAI.NearbyLagrangian.SphereConnectivity.genLoopMap line 219
  23. lemma OAI.NearbyLagrangian.SphereConnectivity.genLoopMap_homotopic line 222
  24. def OAI.NearbyLagrangian.SphereConnectivity.homotopyGroupMap line 227
  25. def OAI.NearbyLagrangian.CubicalSphere.sphereLoop line 243
  26. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_sphereLoop line 248
  27. theorem OAI.NearbyLagrangian.CubicalSphere.sphereMap_natural line 256
  28. theorem OAI.NearbyLagrangian.CubicalSphere.null_iff_class_one line 264
  29. theorem OAI.NearbyLagrangian.CubicalSphere.comp_null_iff_mapped_class_one line 271
  30. def OAI.NearbyLagrangian.CubicalSphere.sphereMovingHomotopy line 294
  31. theorem OAI.NearbyLagrangian.CubicalSphere.exists_based_representative line 327