OAI/Analysis/Commutator/StageGeneration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.TracialGNS.operatorStage line 28
2. def OAI.Kadison.TracialGNS.stageAlgebra line 31
3. lemma OAI.Kadison.TracialGNS.operatorStage_mono line 39
4. lemma OAI.Kadison.TracialGNS.orbit_stageAlgebra line 47
5. theorem OAI.Kadison.TracialGNS.dense_stages_of_bicommutant_generation line 70