OAI/Geometry/Borsuk/Simplicial/Equivariance.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.faceEquiv line 13
2. lemma OAI.BorsukNine.SimplicialChains.faceEquiv_involutive line 19
3. lemma OAI.BorsukNine.SimplicialChains.faceEquiv_free line 28
4. lemma OAI.BorsukNine.SimplicialChains.mapChains_equiv line 33
5. def OAI.BorsukNine.SimplicialChains.cone line 47
6. lemma OAI.BorsukNine.SimplicialChains.cone_simplex line 50
7. lemma OAI.BorsukNine.SimplicialChains.cone_boundary_simplex line 54
8. lemma OAI.BorsukNine.SimplicialChains.cone_boundary_simplex_all line 84
9. lemma OAI.BorsukNine.SimplicialChains.chain_eq_sum line 115
10. lemma OAI.BorsukNine.SimplicialChains.cone_boundary line 120