OAI/Geometry/SingularHomology/SingularChainInclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem340.realSingularChainMap_injective line 11
2. theorem OAI.Problem340.realSingularChainMap_d line 22
3. theorem OAI.Problem340.realSingularChainMap_cycle_iff line 34
4. theorem OAI.Problem340.realSingularChainMap_exists_cycle_lift line 44