OAI/Analysis/Pureness/Traces/TracialStateTopology.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzPureness.TracialState.norm_apply_le_four line 10
2. def OAI.CuntzPureness.TracialState.toWeakDual line 26
3. lemma OAI.CuntzPureness.TracialState.toWeakDual_apply line 30
4. lemma OAI.CuntzPureness.TracialState.toWeakDual_injective line 33
5. instance OAI.CuntzPureness.(instance at line 41) line 41
6. lemma OAI.CuntzPureness.TracialState.isEmbedding_toWeakDual line 44
7. def OAI.CuntzPureness.tracialStateCarrier line 48
8. def OAI.CuntzPureness.tracialStateFromWeakDual line 51
9. lemma OAI.CuntzPureness.range_tracialState_toWeakDual line 64
10. lemma OAI.CuntzPureness.isClosed_tracialStateCarrier line 75
11. lemma OAI.CuntzPureness.isCompact_tracialStateCarrier line 96
12. instance OAI.CuntzPureness.(instance at line 106) line 106
13. lemma OAI.CuntzPureness.TracialState.continuous_eval line 111
14. theorem OAI.CuntzPureness.isCompact_tracialState_univ line 115