OAI/Geometry/Borsuk/Simplicial/FineCrossMap.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.fineCrossMap line 12
2. lemma OAI.BorsukNine.SimplicialChains.fineCrossMap_boundary line 17
3. lemma OAI.BorsukNine.SimplicialChains.fineCrossMap_augmentation line 23
4. lemma OAI.BorsukNine.SimplicialChains.fineCrossMap_norm line 28
5. lemma OAI.BorsukNine.SimplicialChains.fineCrossMap_degree line 34
6. lemma OAI.BorsukNine.SimplicialChains.fineCrossMap_simplex_mesh line 42
7. def OAI.BorsukNine.SimplicialChains.annulus line 49
8. lemma OAI.BorsukNine.SimplicialChains.annulus_compact line 52
9. lemma OAI.BorsukNine.SimplicialChains.hemisphere_vertex_annulus line 59
10. lemma OAI.BorsukNine.SimplicialChains.annular_odd_dimension_bound line 72