OAI/Analysis/Pureness/Operators/SimpleStateGNS.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CuntzPureness.stateGNSVector line 13
  2. lemma OAI.CuntzPureness.stateGNSVector_norm line 15
  3. lemma OAI.CuntzPureness.stateGNS_apply_vector line 23
  4. lemma OAI.CuntzPureness.stateGNS_vector_value line 27
  5. lemma OAI.CuntzPureness.stateGNS_cyclic line 32
  6. lemma OAI.CuntzPureness.stateGNS_nontrivial line 38
  7. theorem OAI.CuntzPureness.simple_stateGNS_injective line 45
  8. def OAI.CuntzPureness.chosenPositiveState line 53
  9. lemma OAI.CuntzPureness.chosenPositiveState_one line 55
  10. abbrev OAI.CuntzPureness.SimpleStateHilbert line 58
  11. instance OAI.CuntzPureness.simpleStateHilbert_nontrivial line 60
  12. def OAI.CuntzPureness.simpleStateGNS line 63
  13. theorem OAI.CuntzPureness.simpleStateGNS_injective line 66
  14. theorem OAI.CuntzPureness.simpleStateGNS_isometry line 70
  15. theorem OAI.CuntzPureness.simpleStateGNS_norm line 75