OAI/Analysis/Commutator/AtomicCoefficients.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.AtomicFactor.Decomposition.support line 22
2. lemma OAI.Kadison.AtomicFactor.Decomposition.support_mem line 24
3. lemma OAI.Kadison.AtomicFactor.Decomposition.support_projection line 27
4. lemma OAI.Kadison.AtomicFactor.Decomposition.support_norm_le line 48
5. lemma OAI.Kadison.AtomicFactor.Decomposition.support_tendsto line 51
6. lemma OAI.Kadison.AtomicFactor.Decomposition.eq_zero_of_coefficients_zero line 54
7. lemma OAI.Kadison.AtomicFactor.Decomposition.eq_of_coefficients_eq line 79