OAI/Geometry/Borsuk/LocalParity/RegularBase.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.baseCoordinates line 18
2. lemma OAI.BorsukNine.Admissible.baseCoordinates_contDiff line 23
3. def OAI.BorsukNine.facetPoint line 30
4. lemma OAI.BorsukNine.facetPoint_apply line 34
5. lemma OAI.BorsukNine.facetPoint_pos line 39
6. lemma OAI.BorsukNine.facetPoint_zero line 46
7. lemma OAI.BorsukNine.facetPoint_sum line 49
8. lemma OAI.BorsukNine.Admissible.exists_regular_facet_point line 59