OAI/Analysis/Pureness/Operators/BundledUniversalGNS.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CuntzPureness.StateHilbertSpace line 8
2. instance OAI.CuntzPureness.stateHilbertNormedAddCommGroup line 10
3. instance OAI.CuntzPureness.stateHilbertInnerProductSpace line 13
4. instance OAI.CuntzPureness.stateHilbertCompleteSpace line 16
5. def OAI.CuntzPureness.stateHilbertRepresentation line 19
6. theorem OAI.CuntzPureness.stateHilbertRepresentation_injective line 23