OAI/Geometry/Borsuk/MatrixGeometry/SignedExtension.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.matrix_images_orthogonal line 18
2. lemma OAI.BorsukNine.Admissible.positiveExtension_orthogonal line 27
3. def OAI.BorsukNine.signedExtension line 39
4. lemma OAI.BorsukNine.signedExtension_odd line 43
5. lemma OAI.BorsukNine.signedExtension_smul_nonneg line 48
6. lemma OAI.BorsukNine.Admissible.signedExtension_sum line 55
7. lemma OAI.BorsukNine.Admissible.signedExtension_abs_sum line 63
8. lemma OAI.BorsukNine.matrix_posPart_continuousOn line 82
9. lemma OAI.BorsukNine.matrix_negPart_continuousOn line 93
10. lemma OAI.BorsukNine.Admissible.signedExtension_continuousOn line 103