OAI/Geometry/Borsuk/Simplicial/UnitRadial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.unitRadial line 10
2. lemma OAI.BorsukNine.SimplicialChains.unitRadial_norm line 13
3. lemma OAI.BorsukNine.SimplicialChains.unitRadial_neg line 18
4. lemma OAI.BorsukNine.SimplicialChains.unitRadial_continuousOn line 21
5. lemma OAI.BorsukNine.SimplicialChains.odd_sphere_dimension_bound line 26
6. def OAI.BorsukNine.SimplicialChains.dropLast line 52
7. lemma OAI.BorsukNine.SimplicialChains.dropLast_zero_iff line 58
8. lemma OAI.BorsukNine.SimplicialChains.dropLast_nonzero line 72
9. lemma OAI.BorsukNine.SimplicialChains.odd_sphere_surjective line 86