OAI/Geometry/Borsuk/Simplicial/OddSphereDimensionBoundFintype.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.odd_sphere_dimension_bound_fintype line 8
2. lemma OAI.BorsukNine.SimplicialChains.odd_sphere_surjective_fintype line 23
3. lemma OAI.BorsukNine.Admissible.label_bound line 51
4. lemma OAI.BorsukNine.Admissible.sphereExtension_surjective line 60
5. lemma OAI.BorsukNine.Admissible.signedExtension_ray line 70