OAI/Geometry/SingularHomology/SphereMayerVietorisEigen.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem340.SphereMayerVietorisEigen.doubling_south_eq_chartSouthPole line 16
2. lemma OAI.Problem340.SphereMayerVietorisEigen.mapsTo_northComplement line 21
3. lemma OAI.Problem340.SphereMayerVietorisEigen.mapsTo_southComplement line 31
4. lemma OAI.Problem340.SphereMayerVietorisEigen.restrictMap_eq_overlapSquare line 41
5. abbrev OAI.Problem340.SphereMayerVietorisEigen.coverFamily line 51
6. lemma OAI.Problem340.SphereMayerVietorisEigen.coverFamily_isOpen line 53
7. lemma OAI.Problem340.SphereMayerVietorisEigen.coverFamily_covers line 58
8. lemma OAI.Problem340.SphereMayerVietorisEigen.iUnion_coverFamily line 66
9. def OAI.Problem340.SphereMayerVietorisEigen.homologyEquivClock line 71
10. theorem OAI.Problem340.SphereMayerVietorisEigen.exists_overlap_square_eigenvector line 78