OAI/Geometry/Borsuk/Support/ActiveChambers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.activeVectors line 13
2. def OAI.BorsukNine.commonPositiveCone line 16
3. lemma OAI.BorsukNine.Admissible.commonPositiveCone_isOpen line 19
4. lemma OAI.BorsukNine.Admissible.commonPositiveCone_safe line 27
5. lemma OAI.BorsukNine.Admissible.commonPositiveCone_interior_safe line 35
6. lemma OAI.BorsukNine.commonPositiveCone_active line 41
7. lemma OAI.BorsukNine.commonPositiveCone_ne_zero line 47
8. lemma OAI.BorsukNine.activeChamber_inner_pos line 55
9. lemma OAI.BorsukNine.Admissible.safe_restriction_zero line 63
10. lemma OAI.BorsukNine.Admissible.safe_restriction line 74