OAI/Analysis/Commutator/SeparableSmall.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Kadison.SeparableSmall.small line 21
2. abbrev OAI.Kadison.SeparableSmall.Model line 27
3. instance OAI.Kadison.SeparableSmall.model_inner line 29
4. def OAI.Kadison.SeparableSmall.unitary line 42
5. instance OAI.Kadison.SeparableSmall.model_complete line 46
6. instance OAI.Kadison.SeparableSmall.model_separable line 49