OAI/Analysis/Commutator/PartialDecomposition.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Kadison.PartialIsometryOrder.PartialDecomposition line 22
2. theorem OAI.Kadison.PartialIsometryOrder.exists_partialDecomposition line 29
3. def OAI.Kadison.PartialIsometryOrder.PartialDecomposition.support line 69
4. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.support_projection line 71
5. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.support_norm_le line 89
6. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.support_tendsto line 92
7. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.eq_zero_of_coefficients_zero line 95
8. lemma OAI.Kadison.PartialIsometryOrder.PartialDecomposition.eq_of_coefficients_eq line 124