OAI/Geometry/Borsuk/Simplicial/Coefficients.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.degreeChains_card_of_ne_zero line 13
2. lemma OAI.BorsukNine.SimplicialChains.simplex_coeff line 19
3. lemma OAI.BorsukNine.SimplicialChains.boundary_simplex_coeff line 30
4. def OAI.BorsukNine.SimplicialChains.crossFacet line 58
5. lemma OAI.BorsukNine.SimplicialChains.mem_crossFacet line 61
6. lemma OAI.BorsukNine.SimplicialChains.crossFacet_card line 67
7. lemma OAI.BorsukNine.SimplicialChains.crossFacet_mem line 73
8. lemma OAI.BorsukNine.SimplicialChains.cross_top_exists_signs line 86