OAI/Geometry/Borsuk/Simplicial/DoubleEraseSumFun.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.double_erase_sum_fun line 11
2. lemma OAI.BorsukNine.SimplicialChains.support_mapSimplex line 39
3. lemma OAI.BorsukNine.SimplicialChains.mapSimplex_degree line 48
4. lemma OAI.BorsukNine.SimplicialChains.mapSimplex_boundary line 55
5. lemma OAI.BorsukNine.SimplicialChains.mapSimplex_augmentation line 70
6. def OAI.BorsukNine.SimplicialChains.contigSimplex line 81
7. lemma OAI.BorsukNine.SimplicialChains.contigSimplex_empty line 90
8. lemma OAI.BorsukNine.SimplicialChains.contigSimplex_nonempty line 93
9. lemma OAI.BorsukNine.SimplicialChains.contigSimplex_carrier line 101
10. lemma OAI.BorsukNine.SimplicialChains.contigSimplex_degree line 124
11. lemma OAI.BorsukNine.SimplicialChains.contigSimplex_augmentation line 139