OAI/Geometry/SingularHomology/HomologyZero.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem340.realSingularHomologyZeroEquiv line 11
  2. def OAI.Problem340.pointHomologyClass line 15
  3. theorem OAI.Problem340.pointHomologyClass_ne_zero line 20
  4. theorem OAI.Problem340.realHomologyMap_pointHomologyClass line 34
  5. theorem OAI.Problem340.exists_realHomology_eigenvector_one line 50
  6. theorem OAI.Problem340.realHomologyMap_zero_eq_id line 57
  7. theorem OAI.Problem340.pathConnectedSpace_standardClock line 80
  8. theorem OAI.Problem340.pathConnectedSpace_standardSphere2 line 87
  9. theorem OAI.Problem340.pathConnectedSpace_counterexampleManifold line 94
  10. theorem OAI.Problem340.counterexampleManifold_homologyZero_eigenvector line 100
  11. theorem OAI.Problem340.finiteDimensional_realSingularHomologyZero line 107
  12. theorem OAI.Problem340.finrank_realSingularHomologyZero line 112
  13. theorem OAI.Problem340.one_mem_homologyRadiusSet line 117