OAI/Geometry/Borsuk/Simplicial/NormMap.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.normMap line 12
2. lemma OAI.BorsukNine.SimplicialChains.normMap_eq line 15
3. lemma OAI.BorsukNine.SimplicialChains.boundary_normMap line 21
4. lemma OAI.BorsukNine.SimplicialChains.augmentation_normMap line 28
5. lemma OAI.BorsukNine.SimplicialChains.antipodal_tower_augmentation_zero line 36
6. def OAI.BorsukNine.SimplicialChains.degreeChains line 50
7. lemma OAI.BorsukNine.SimplicialChains.simplex_mem_degree line 54
8. lemma OAI.BorsukNine.SimplicialChains.grade_map line 60
9. lemma OAI.BorsukNine.SimplicialChains.mapChains_degree line 72
10. lemma OAI.BorsukNine.SimplicialChains.degreeChains_eq_bot_of_card_bound line 84
11. lemma OAI.BorsukNine.SimplicialChains.augmentation_eq_zero_of_degree line 94