OAI/Geometry/Borsuk/Simplicial/Approximation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.approximation line 11
2. def OAI.BorsukNine.SimplicialChains.IsFineLabel line 15
3. lemma OAI.BorsukNine.SimplicialChains.approximation_boundary line 20
4. lemma OAI.BorsukNine.SimplicialChains.approximation_augmentation line 39
5. lemma OAI.BorsukNine.SimplicialChains.approximation_norm line 54
6. lemma OAI.BorsukNine.SimplicialChains.approximation_degree line 68
7. lemma OAI.BorsukNine.SimplicialChains.cross_equivariant_fundamental line 73
8. lemma OAI.BorsukNine.SimplicialChains.approximation_odd_fundamental line 90
9. lemma OAI.BorsukNine.SimplicialChains.exists_fine_sphereLabel line 99
10. lemma OAI.BorsukNine.SimplicialChains.odd_sphere_simplicial_degree line 125
11. lemma OAI.BorsukNine.SimplicialChains.approximation_agree_top line 136