OAI/Geometry/Borsuk/Support/SpectralSupport.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.signedExtension_pos_iff line 14
2. lemma OAI.BorsukNine.Admissible.signedExtension_neg_iff line 28
3. lemma OAI.BorsukNine.Admissible.signedExtension_positive_support line 43
4. lemma OAI.BorsukNine.Admissible.signedExtension_negative_support line 49
5. lemma OAI.BorsukNine.Admissible.positiveExtension_range_mono line 55
6. lemma OAI.BorsukNine.rankOne_range line 63
7. lemma OAI.BorsukNine.Admissible.signedExtension_range_labels line 76
8. lemma OAI.BorsukNine.subspace_eq_span_of_inner_separates line 88
9. lemma OAI.BorsukNine.Admissible.positive_range_separated line 100