OAI/Geometry/Borsuk/Simplicial/CrossEmbedding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.crossEmbedding line 11
2. lemma OAI.BorsukNine.SimplicialChains.crossEmbedding_norm line 14
3. lemma OAI.BorsukNine.SimplicialChains.crossEmbedding_flip line 19
4. lemma OAI.BorsukNine.SimplicialChains.crossEmbedding_inner_ne line 24
5. lemma OAI.BorsukNine.SimplicialChains.crossEmbedding_inner_self line 29
6. lemma OAI.BorsukNine.SimplicialChains.crossEmbedding_face line 34
7. def OAI.BorsukNine.SimplicialChains.crossGeometricMap line 50
8. lemma OAI.BorsukNine.SimplicialChains.crossGeometricMap_boundary line 55
9. lemma OAI.BorsukNine.SimplicialChains.crossGeometricMap_augmentation line 60
10. lemma OAI.BorsukNine.SimplicialChains.crossGeometricMap_degree line 64
11. lemma OAI.BorsukNine.SimplicialChains.crossGeometricMap_norm line 68