OAI/Analysis/Pureness/Comparison/OrthogonalSupportMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CuntzComparison.hereditary_positive_pair_mul_eq_zero line 10
2. lemma OAI.CuntzComparison.positive_le_one_of_square_le line 17
3. lemma OAI.CuntzComparison.supportApprox_square_le line 26
4. lemma OAI.CuntzComparison.orthogonal_supportApprox_sum_le_one line 38
5. theorem OAI.CuntzComparison.TracialState.orthogonal_support_mass_sum_le_one line 63