OAI/Geometry/Borsuk/Support/Chambers.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.safeNormals line 10
2. def OAI.BorsukNine.signChamber line 12
3. lemma OAI.BorsukNine.mem_signChamber_self line 14
4. lemma OAI.BorsukNine.signChamber_subset_safeNormals line 19
5. lemma OAI.BorsukNine.signChamber_convex line 24
6. lemma OAI.BorsukNine.signChamber_eq_of_mem line 39
7. lemma OAI.BorsukNine.signChamber_eq_or_disjoint line 59
8. lemma OAI.BorsukNine.interior_safe_mem_chamber line 68
9. lemma OAI.BorsukNine.interior_safe_mem_own_chamber line 84
10. lemma OAI.BorsukNine.signChamber_interior_pairwise line 88
11. lemma OAI.BorsukNine.compact_finite_chambers line 99