OAI/Geometry/Borsuk/Simplicial/MaxIndex.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.maxIndex line 9
2. lemma OAI.BorsukNine.SimplicialChains.maxIndex_le line 12
3. def OAI.BorsukNine.SimplicialChains.peakIndex line 16
4. lemma OAI.BorsukNine.SimplicialChains.peakIndex_neg line 19
5. lemma OAI.BorsukNine.SimplicialChains.euclidean_norm_le_sum_abs line 26
6. lemma OAI.BorsukNine.SimplicialChains.peak_large line 36
7. def OAI.BorsukNine.SimplicialChains.sphereLabel line 47
8. lemma OAI.BorsukNine.SimplicialChains.sphereLabel_bound line 50
9. lemma OAI.BorsukNine.SimplicialChains.sphereLabel_neg line 53
10. lemma OAI.BorsukNine.SimplicialChains.sphereLabel_compatible line 70