OAI/Geometry/Borsuk/Support/DisjointChambers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BorsukNine.compact_disjoint_chambers line 10
2. lemma OAI.BorsukNine.toEuclideanLin_mul line 46
3. def OAI.BorsukNine.isometryMatrix line 56
4. lemma OAI.BorsukNine.isometryMatrix_action line 60
5. lemma OAI.BorsukNine.isometryMatrix_star_mul line 64
6. def OAI.BorsukNine.matrixEmbed line 76
7. lemma OAI.BorsukNine.matrixEmbed_nonneg line 82
8. lemma OAI.BorsukNine.matrixEmbed_trace line 85
9. lemma OAI.BorsukNine.matrixEmbed_action line 90
10. lemma OAI.BorsukNine.matrixEmbed_kernel line 106