OAI/Geometry/Borsuk/Simplicial/EventuallyFineSphereLabel.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.SimplicialChains.eventually_fine_sphereLabel line 11
2. lemma OAI.BorsukNine.SimplicialChains.eventually_odd_sphere_degree line 32
3. lemma OAI.BorsukNine.SimplicialChains.unitRadial_of_norm_one line 43
4. lemma OAI.BorsukNine.SimplicialChains.normalized_homotopy_chains line 46
5. lemma OAI.BorsukNine.SimplicialChains.convex_combination_ne_zero line 58
6. lemma OAI.BorsukNine.SimplicialChains.hemispheric_homotopy_chains line 71