OAI/Analysis/Pureness/States/RegularizedStateCStarValue.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.regularizedStateCauchyEmbedding_isometry line 12
2. lemma OAI.CuntzPureness.normalizedStateCauchyValue_continuous line 17
3. lemma OAI.CuntzPureness.normalizedStateCauchyValue_square_eq_zero_iff line 20
4. lemma OAI.CuntzPureness.normalizedStateCauchyValue_cfc_add line 31
5. lemma OAI.CuntzPureness.regularizedStateCauchyQuotient_finite line 39
6. lemma OAI.CuntzPureness.normalizedStateCStarValue_internal_root_rank line 43