OAI/Geometry/Borsuk/Support/FullSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.Admissible.positiveExtension_kernel line 17
2. lemma OAI.BorsukNine.Admissible.signedExtension_kernel line 27
3. lemma OAI.BorsukNine.Admissible.signedExtension_kernel_eq_zero line 38
4. lemma OAI.BorsukNine.Admissible.signedExtension_fullSupport line 47
5. lemma OAI.BorsukNine.matrix_psd_trace_zero line 58
6. lemma OAI.BorsukNine.Admissible.signedExtension_negativeDefinite line 67