OAI/Geometry/Borsuk/Simplicial/SignVector.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.SimplicialChains.signVector line 9
2. lemma OAI.BorsukNine.SimplicialChains.signVector_apply line 12
3. lemma OAI.BorsukNine.SimplicialChains.signVector_norm line 15
4. def OAI.BorsukNine.SimplicialChains.facetCenter line 23
5. lemma OAI.BorsukNine.SimplicialChains.facetCenter_norm line 26
6. lemma OAI.BorsukNine.SimplicialChains.facetCenter_region line 30
7. lemma OAI.BorsukNine.SimplicialChains.all_labelRegions_iff_center line 42
8. lemma OAI.BorsukNine.SimplicialChains.constant_approximation_facet_zero line 71
9. lemma OAI.BorsukNine.SimplicialChains.continuous_missed_facet_zero line 101