OAI/Geometry/Borsuk/Simplicial/CharacteristicDegree.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.characteristicAugmentation line 17
2. lemma OAI.BorsukNine.SimplicialChains.normMap_exact line 22
3. def OAI.BorsukNine.SimplicialChains.characteristicDegree line 27
4. lemma OAI.BorsukNine.SimplicialChains.characteristicDegree_natural line 42
5. lemma OAI.BorsukNine.SimplicialChains.characteristicDegree_vanish_of_equivariant_projection line 62
6. def OAI.BorsukNine.SimplicialChains.crossFundamental line 85
7. lemma OAI.BorsukNine.SimplicialChains.crossFundamental_norm line 88
8. lemma OAI.BorsukNine.SimplicialChains.crossFundamental_boundary line 91
9. lemma OAI.BorsukNine.SimplicialChains.crossFundamental_degree line 95
10. lemma OAI.BorsukNine.SimplicialChains.characteristicCochain_crossTower line 103
11. lemma OAI.BorsukNine.SimplicialChains.characteristicDegree_crossFundamental line 115
12. lemma OAI.BorsukNine.SimplicialChains.cross_equivariant_degree_one line 122