OAI/Analysis/Commutator/UnitaryOrbitHull.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.UnitaryOrbit.conjugate line 20
2. def OAI.Kadison.UnitaryOrbit.conjugateLinear line 23
3. def OAI.Kadison.UnitaryOrbit.hull line 28
4. lemma OAI.Kadison.UnitaryOrbit.hull_self line 31
5. lemma OAI.Kadison.UnitaryOrbit.conjugate_mul line 35
6. lemma OAI.Kadison.UnitaryOrbit.conjugate_mem_hull line 43
7. lemma OAI.Kadison.UnitaryOrbit.hull_distance line 53
8. lemma OAI.Kadison.UnitaryOrbit.hull_norm line 63
9. lemma OAI.Kadison.UnitaryOrbit.midpoint_mem line 70