OAI/Analysis/KadisonKastler/TypeIIISeparatingVector.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A separating unit vector in any separable type III representation

Every nonzero vector-state support is equivalent to the identity. Moving the vector through that equivalence makes its state faithful on the original represented algebra.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_separating_unit_vector line 22