OAI/Geometry/Borsuk/Projectors/FinitePatch.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.finitePatch line 13
2. lemma OAI.BorsukNine.finitePatch_continuous line 16
3. lemma OAI.BorsukNine.finitePatch_zero line 25
4. lemma OAI.BorsukNine.finitePatch_of_all_zero line 28
5. lemma OAI.BorsukNine.finitePatch_of_disjoint line 32
6. lemma OAI.BorsukNine.finitePatch_one_of_disjoint line 43
7. lemma OAI.BorsukNine.finitePatch_cases line 50
8. lemma OAI.BorsukNine.finitePatch_ne_zero line 64