OAI/Analysis/Commutator/WOTCompact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.WOTDistance.normBall line 20
2. lemma OAI.Kadison.WOTDistance.isCompact_normBall line 22
3. lemma OAI.Kadison.WOTDistance.isClosed_normBall line 48
4. lemma OAI.Kadison.WOTDistance.convex_normBall line 52
5. def OAI.Kadison.WOTDistance.commutant line 61
6. lemma OAI.Kadison.WOTDistance.isClosed_commutant line 73
7. lemma OAI.Kadison.WOTDistance.isClosed_commutant_add_ball line 83