OAI/Analysis/KadisonKastler/ReferenceStrongLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A bounded algebra sequence converging on a separating vector

Weak compactness supplies an operator in the algebra. Completeness on the separating reference vector and the dense commutant orbit identify the strong limit on the whole original Hilbert space.

  1. theorem OAI.KadisonKastler.exists_algebra_strong_limit_of_reference_cauchy line 23