OAI/Geometry/Borsuk/MatrixGeometry/PositiveSlice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BorsukNine.unflattenMatrix line 11
2. def OAI.BorsukNine.flatGram line 16
3. lemma OAI.BorsukNine.flatGram_nonneg line 20
4. lemma OAI.BorsukNine.flatGram_trace line 24
5. lemma OAI.BorsukNine.flatGram_continuous line 32
6. lemma OAI.BorsukNine.positive_slice_image line 36
7. lemma OAI.BorsukNine.positive_slice_compact line 54