OAI/Analysis/Commutator/PartialUnitaryCompletion.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.FinitePatching.PartialUnitary.ofUnitary line 19
2. def OAI.Kadison.FinitePatching.PartialUnitary.complement line 28
3. lemma OAI.Kadison.FinitePatching.PartialUnitary.support_complement_zero line 38
4. def OAI.Kadison.FinitePatching.PartialUnitary.completed line 42
5. lemma OAI.Kadison.FinitePatching.PartialUnitary.completed_val line 45
6. lemma OAI.Kadison.FinitePatching.PartialUnitary.completed_support line 48
7. lemma OAI.Kadison.FinitePatching.PartialUnitary.le_completed line 52
8. def OAI.Kadison.FinitePatching.PartialUnitary.completion line 54
9. lemma OAI.Kadison.FinitePatching.PartialUnitary.completion_val line 58
10. lemma OAI.Kadison.FinitePatching.PartialUnitary.ofUnitary_completion line 61
11. lemma OAI.Kadison.FinitePatching.PartialUnitary.completion_norm_sub line 65
12. lemma OAI.Kadison.FinitePatching.PartialUnitary.completed_mem line 71