OAI/Geometry/Borsuk/Simplicial/GeneralTarget.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.fineMap line 12
2. def OAI.BorsukNine.SimplicialChains.FineTo line 16
3. lemma OAI.BorsukNine.SimplicialChains.fineMap_boundary line 21
4. lemma OAI.BorsukNine.SimplicialChains.fineMap_degree line 39
5. lemma OAI.BorsukNine.SimplicialChains.mapChains_id line 45
6. lemma OAI.BorsukNine.SimplicialChains.normMap_id line 56
7. lemma OAI.BorsukNine.SimplicialChains.fineMap_even_norm line 61
8. def OAI.BorsukNine.SimplicialChains.projectiveCycle line 75
9. lemma OAI.BorsukNine.SimplicialChains.projectiveCycle_degree line 79
10. lemma OAI.BorsukNine.SimplicialChains.projectiveCycle_boundary line 85