OAI/Analysis/KadisonKastler/PositiveConeFaithfulUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Faithful vector states determine their positive representatives

Cyclicity follows from separation and the fixed-conjugation property. Equality of the vector functionals then supplies a commutant unitary, whose positive orbit has only one point.

  1. theorem OAI.KadisonKastler.separating_of_vectorState_eq line 23
  2. theorem OAI.KadisonKastler.positiveCone_faithful_state_unique line 38