OAI/Geometry/Borsuk/MatrixGeometry/MatrixKernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.matrix_abs_action_norm_sq line 19
2. lemma OAI.BorsukNine.matrix_abs_kernel line 24
3. lemma OAI.BorsukNine.matrix_parts_kernel line 30
4. lemma OAI.BorsukNine.matrix_image_orthogonal_kernel line 44
5. def OAI.BorsukNine.positiveExtension line 57
6. lemma OAI.BorsukNine.Admissible.positiveExtension_nonneg line 61
7. lemma OAI.BorsukNine.Admissible.positiveExtension_sum line 65
8. lemma OAI.BorsukNine.Admissible.positiveExtension_continuousOn line 74
9. lemma OAI.BorsukNine.positiveExtension_smul_nonneg line 82
10. lemma OAI.BorsukNine.Admissible.positiveExtension_support line 89