OAI/Geometry/SingularHomology/SkewProductHomology.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.rawSphereSection line 10
2. def OAI.Problem340.rawSphereProjection line 13
3. def OAI.Problem340.rawSphereSquare line 15
4. theorem OAI.Problem340.continuous_rawSphereSection line 18
5. theorem OAI.Problem340.continuous_rawSphereProjection line 21
6. theorem OAI.Problem340.continuous_rawSphereSquare line 24
7. theorem OAI.Problem340.rawSphereProjection_section line 29
8. theorem OAI.Problem340.rawNormalForm_section line 32
9. theorem OAI.Problem340.realHomologyMap_rawUpdate_eq_normalForm line 35
10. theorem OAI.Problem340.rawUpdate_eigenvector_of_sphere line 43