OAI/Geometry/Borsuk/Projectors/CoordinateSum.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.coordinateSum line 8
2. lemma OAI.BorsukNine.coordinateSum_apply line 14
3. def OAI.BorsukNine.uniformVector line 17
4. lemma OAI.BorsukNine.coordinateSum_uniform line 20
5. def OAI.BorsukNine.zeroSumProjection line 26
6. def OAI.BorsukNine.simplexProjection line 30
7. lemma OAI.BorsukNine.simplexProjection_sum line 33
8. lemma OAI.BorsukNine.simplexProjection_fixed line 39
9. lemma OAI.BorsukNine.simplexProjection_sub_fixed line 44
10. lemma OAI.BorsukNine.continuous_simplex_approx line 55