OAI/Analysis/Commutator/CountableStarHomTests.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Kadison.CStarContractions line 24
2. instance OAI.Kadison.contraction_nonempty line 26
3. def OAI.Kadison.countableContractions line 28
4. lemma OAI.Kadison.countableContractions_norm line 32
5. lemma OAI.Kadison.countableContractions_approx line 36
6. theorem OAI.Kadison.countableContractions_strong_dense line 42