OAI/Analysis/Pureness/Tensor/CauchySpatialNullDescent.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchySpatialAmbientSequence_one line 26
2. def OAI.CuntzPureness.PositiveQuasitrace.cauchySpatialAmbientSequenceHom line 33
3. def OAI.CuntzPureness.PositiveQuasitrace.cauchySpatialAmbientQuotient line 48
4. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchySpatialAmbientQuotient_null_tensor line 54
5. lemma OAI.CuntzPureness.PositiveQuasitrace.cauchySpatialAmbientQuotient_ideal_zero line 70