OAI/Analysis/Pureness/Operators/ContinuousPositiveEmbedding.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.continuousNNRealComplex line 11
2. def OAI.CuntzPureness.continuousNNRealPositive line 14
3. lemma OAI.CuntzPureness.continuousNNRealPositive_add line 20
4. lemma OAI.CuntzPureness.continuousNNRealPositive_zero line 28
5. lemma OAI.CuntzPureness.continuousNNRealPositive_mono line 35
6. lemma OAI.CuntzPureness.continuousNNRealPositive_mul_zero line 40
7. lemma OAI.CuntzPureness.continuousNNRealPositive_cut line 48