OAI/Analysis/Commutator/PositiveExtensionComplex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Kadison.PositiveExtension.saInclusion line 18
2. lemma OAI.Kadison.PositiveExtension.positive_selfAdjoint_im line 23
3. def OAI.Kadison.PositiveExtension.realRestriction line 36
4. lemma OAI.Kadison.PositiveExtension.realRestriction_apply line 40
5. def OAI.Kadison.PositiveExtension.complexify line 43
6. lemma OAI.Kadison.PositiveExtension.complexify_apply line 47
7. lemma OAI.Kadison.PositiveExtension.complexify_selfAdjoint line 52
8. lemma OAI.Kadison.PositiveExtension.complexify_nonneg line 55
9. def OAI.Kadison.PositiveExtension.complexifyPositive line 63
10. lemma OAI.Kadison.PositiveExtension.realPart_mem line 74
11. lemma OAI.Kadison.PositiveExtension.imaginaryPart_mem line 80
12. theorem OAI.Kadison.PositiveExtension.exists_positive_extension line 85