OAI/Geometry/Borsuk/Projectors/SimplexPoint.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.simplexPoint line 8
2. def OAI.BorsukNine.simplexInterior line 11
3. lemma OAI.BorsukNine.simplexInterior_isOpen line 14
4. lemma OAI.BorsukNine.simplexInterior_nonempty line 22
5. lemma OAI.BorsukNine.simplexPoint_pos line 32
6. lemma OAI.BorsukNine.simplexPoint_sum line 39
7. lemma OAI.BorsukNine.simplexPoint_succ line 44