OAI/Analysis/JiangSu/Traces/FaithfulTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. class OAI.UnitalTomsWinter.IsSimpleCStarAlgebra line 13
2. def OAI.UnitalTomsWinter.TracialState.nullIdeal line 20
3. theorem OAI.UnitalTomsWinter.TracialState.mem_nullIdeal line 41
4. theorem OAI.UnitalTomsWinter.TracialState.isClosed_nullIdeal line 44
5. theorem OAI.UnitalTomsWinter.TracialState.one_not_mem_nullIdeal line 51
6. theorem OAI.UnitalTomsWinter.TracialState.nullIdeal_eq_bot line 54
7. theorem OAI.UnitalTomsWinter.TracialState.twoNorm_eq_zero_iff line 60
8. theorem OAI.UnitalTomsWinter.TracialState.faithful line 64
9. theorem OAI.UnitalTomsWinter.uniformTwoNorm_eq_zero_iff line 71