OAI/Analysis/KadisonKastler/PureStateExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Pure-state extensions along unital star embeddings

The set of state extensions is weak-star compact. If the original state is pure, an extreme point of this set is pure on the larger algebra. This supplies state extensions used in the derivation construction.

  1. theorem OAI.KadisonKastler.exists_state_extension_of_embedding line 22
  2. theorem OAI.KadisonKastler.exists_pure_state_extension line 48