OAI/Analysis/Commutator/NormalGNS.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.NormalGNS.BoundedWOTContinuous line 29
2. lemma OAI.Kadison.NormalGNS.tendsto_trace line 33
3. theorem OAI.Kadison.NormalGNS.vector_unitball_isClosed line 50
4. lemma OAI.Kadison.NormalGNS.eq_of_vacuum line 88
5. theorem OAI.Kadison.NormalGNS.bicommutant_selfAdjoint_contraction line 98
6. theorem OAI.Kadison.NormalGNS.range_bicommutant line 115