OAI/Geometry/SingularHomology/CoordinateHomology.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.sphereCoordinate line 11
  2. def OAI.Problem340.sphereCoordinateSection line 14
  3. theorem OAI.Problem340.continuous_sphereCoordinate line 19
  4. theorem OAI.Problem340.continuous_sphereCoordinateSection line 24
  5. theorem OAI.Problem340.sphereCoordinate_section line 38
  6. theorem OAI.Problem340.sphereCoordinate_leftInverse line 43
  7. theorem OAI.Problem340.sphereCoordinate_surjective line 48
  8. theorem OAI.Problem340.sphereCoordinateSection_injective line 52
  9. def OAI.Problem340.sphereCoordinateModel line 57
  10. theorem OAI.Problem340.continuous_sphereCoordinateModel line 63
  11. theorem OAI.Problem340.sphereCoordinateModel_section line 76
  12. theorem OAI.Problem340.sphereCoordinate_model line 84
  13. def OAI.Problem340.sphereAntipode line 91
  14. theorem OAI.Problem340.sphereAntipode_ne line 95
  15. theorem OAI.Problem340.sphereCoordinateModel_not_injective line 109
  16. theorem OAI.Problem340.sphereCoordinateModel_not_bijective line 127
  17. theorem OAI.Problem340.realHomologyMap_sphereCoordinate_surjective line 133
  18. theorem OAI.Problem340.realHomologyMap_sphereCoordinateSection_injective line 141
  19. theorem OAI.Problem340.realHomologyMap_sphereCoordinate_ne_zero line 150
  20. theorem OAI.Problem340.sphereCoordinateModel_homology_eigenvector line 160
  21. theorem OAI.Problem340.homology_eigenvector_of_homotopy_model line 184