OAI/Analysis/Pureness/Tensor/SpatialVectorSlice.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.spatialRightVector line 12
2. lemma OAI.CuntzPureness.spatialRightVector_norm_le line 23
3. def OAI.CuntzPureness.algebraicSpatialSlice line 26
4. lemma OAI.CuntzPureness.algebraicSpatialSlice_tmul line 35
5. lemma OAI.CuntzPureness.algebraicSpatialSlice_compression line 38
6. lemma OAI.CuntzPureness.algebraicSpatialSlice_norm_le line 56
7. def OAI.CuntzPureness.spatialVectorSlice line 76
8. lemma OAI.CuntzPureness.spatialVectorSlice_tensor line 80
9. lemma OAI.CuntzPureness.spatialVectorSlice_norm_le line 86