OAI/Analysis/KadisonKastler/PositiveConeStateUniqueness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniqueness of a cyclic positive representative of the reference state

Equality of vector functionals constructs the intertwining unitary. Positivity then forces that unitary to fix the reference vector.

  1. theorem OAI.KadisonKastler.positiveCone_eq_of_vectorState_eq line 23
  2. theorem OAI.KadisonKastler.canonicalPositiveCone_eq_of_vectorState_eq line 42