OAI/Analysis/Commutator/WeakDualHull.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.WeakDualHull.hull line 21
2. lemma OAI.Kadison.WeakDualHull.subset_hull line 23
3. lemma OAI.Kadison.WeakDualHull.convex_hull line 26
4. lemma OAI.Kadison.WeakDualHull.eval_norm_le line 29
5. lemma OAI.Kadison.WeakDualHull.norm_le line 46
6. lemma OAI.Kadison.WeakDualHull.compact_hull line 54
7. lemma OAI.Kadison.WeakDualHull.eval_eq line 60
8. lemma OAI.Kadison.WeakDualHull.eval_nonneg line 70