OAI/Geometry/SingularHomology/ActualSingularSubdivisionMap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChain_boundaryCompatible line 12
2. def OAI.Problem340.ActualSingularSubdivision.subdivisionChainMap line 17
3. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChainMap_f line 22
4. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChainMap_zero line 26
5. def OAI.Problem340.ActualSingularSubdivision.subdivisionChainHomotopy line 32
6. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChainHomotopy_naturality line 38
7. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChainMap_homologyMap_eq_id line 46
8. theorem OAI.Problem340.ActualSingularSubdivision.subdivisionChainMap_generator line 52
9. abbrev OAI.Problem340.ActualSingularSubdivision.chainMap line 60
10. abbrev OAI.Problem340.ActualSingularSubdivision.chainHomotopy line 66