OAI/Analysis/Commutator/WOTBallSeparable.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.WOTDistance.isClosed_vonNeumann line 20
2. abbrev OAI.Kadison.WOTDistance.AlgebraBall line 35
3. lemma OAI.Kadison.WOTDistance.compact_algebraBall line 38
4. theorem OAI.Kadison.WOTDistance.secondCountable_algebraBall line 43