OAI/Analysis/Pureness/Comparison/FaithfulTrace.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. class OAI.CuntzComparison.IsSimpleCStarAlgebra line 9
2. def OAI.CuntzComparison.TracialState.nullIdeal line 16
3. theorem OAI.CuntzComparison.TracialState.mem_nullIdeal line 37
4. theorem OAI.CuntzComparison.TracialState.isClosed_nullIdeal line 40
5. theorem OAI.CuntzComparison.TracialState.one_not_mem_nullIdeal line 47
6. theorem OAI.CuntzComparison.TracialState.nullIdeal_eq_bot line 50
7. theorem OAI.CuntzComparison.TracialState.twoNorm_eq_zero_iff line 56
8. theorem OAI.CuntzComparison.TracialState.faithful line 60
9. theorem OAI.CuntzComparison.uniformTwoNorm_eq_zero_iff line 67