OAI/Analysis/Pureness/Operators/UniversalStateGNS.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.PositiveStateIndex line 12
2. abbrev OAI.CuntzPureness.UniversalStateHilbert line 14
3. def OAI.CuntzPureness.universalStateGNS line 16
4. lemma OAI.CuntzPureness.universalStateGNS_apply line 20
5. theorem OAI.CuntzPureness.universalStateGNS_injective line 23
6. lemma OAI.CuntzPureness.universalStateGNS_isometry line 37
7. lemma OAI.CuntzPureness.universalStateGNS_norm line 41
8. def OAI.CuntzPureness.universalStateGNSInclusion line 45
9. lemma OAI.CuntzPureness.universalStateGNSInclusion_intertwines line 52
10. lemma OAI.CuntzPureness.universalStateGNS_vector_value line 66