OAI/Geometry/Borsuk/Simplicial/SignedVertex.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BorsukNine.SimplicialChains.SignedVertex line 9
2. def OAI.BorsukNine.SimplicialChains.flip line 11
3. lemma OAI.BorsukNine.SimplicialChains.flip_apply line 14
4. lemma OAI.BorsukNine.SimplicialChains.flip_involutive line 16
5. lemma OAI.BorsukNine.SimplicialChains.flip_ne line 20
6. def OAI.BorsukNine.SimplicialChains.cross line 24
7. lemma OAI.BorsukNine.SimplicialChains.cross_mem line 32
8. lemma OAI.BorsukNine.SimplicialChains.cross_flip_forward line 36
9. lemma OAI.BorsukNine.SimplicialChains.cross_flip line 47
10. lemma OAI.BorsukNine.SimplicialChains.cross_free line 56
11. lemma OAI.BorsukNine.SimplicialChains.cross_card line 63
12. lemma OAI.BorsukNine.SimplicialChains.cross_singleton line 72
13. lemma OAI.BorsukNine.SimplicialChains.cross_insert line 78
14. lemma OAI.BorsukNine.SimplicialChains.support_mapChains_injective line 97
15. lemma OAI.BorsukNine.SimplicialChains.normMap_sq line 107
16. lemma OAI.BorsukNine.SimplicialChains.normMap_degree line 113
17. def OAI.BorsukNine.SimplicialChains.crossTower line 119
18. lemma OAI.BorsukNine.SimplicialChains.crossTower_support line 123
19. lemma OAI.BorsukNine.SimplicialChains.crossTower_degree line 149
20. lemma OAI.BorsukNine.SimplicialChains.crossTower_cone_faces line 156
21. lemma OAI.BorsukNine.SimplicialChains.crossTower_norm_boundary line 173
22. lemma OAI.BorsukNine.SimplicialChains.crossTower_boundary line 199
23. lemma OAI.BorsukNine.SimplicialChains.crossTower_augmentation line 210