OAI/Analysis/Commutator/PartialUnitaryOrder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Kadison.FinitePatching.PartialUnitary.ext line 20
2. instance OAI.Kadison.FinitePatching.PartialUnitary.(instance at line 28) line 28
3. lemma OAI.Kadison.FinitePatching.PartialUnitary.le_def line 44
4. lemma OAI.Kadison.FinitePatching.PartialUnitary.star_mul_of_le line 47
5. lemma OAI.Kadison.FinitePatching.PartialUnitary.mul_star_of_le line 55
6. lemma OAI.Kadison.FinitePatching.PartialUnitary.support_mul_of_le line 61
7. lemma OAI.Kadison.FinitePatching.PartialUnitary.star_sub_mul_sub line 65
8. lemma OAI.Kadison.FinitePatching.PartialUnitary.norm_sub_sq line 73
9. lemma OAI.Kadison.FinitePatching.PartialUnitary.le_add line 77
10. lemma OAI.Kadison.FinitePatching.PartialUnitary.zero_le line 84