OAI/Analysis/KadisonKastler/InvariantStateExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Invariant extensions preserving prescribed state values

The abelian action is averaged as a discrete group. No continuity or normality of the initial ambient state is needed.

  1. theorem OAI.KadisonKastler.exists_invariant_state_preserving_values line 20