OAI/Analysis/Commutator/TracialGNSCorners.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.VectorGNS.subtype_corner line 29
2. def OAI.Kadison.VectorGNS.CornerCommutatorBound line 36
3. abbrev OAI.Kadison.TracialSequence.gnsCompression line 55
4. lemma OAI.Kadison.TracialSequence.represented_commutes line 62
5. lemma OAI.Kadison.TracialSequence.gnsCompression_commutes line 85
6. lemma OAI.Kadison.TracialSequence.small_represented_corner_bound line 101
7. theorem OAI.Kadison.TracialSequence.gns_small_corner_bound line 131