OAI/Analysis/Commutator/HilbertStrong.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Kadison.StrongContinuity.completion line 25
  2. lemma OAI.Kadison.StrongContinuity.tensor line 32
  3. lemma OAI.Kadison.StrongContinuity.hilbertSum line 44
  4. lemma OAI.Kadison.PreHilbert.powerMap_continuous line 65
  5. lemma OAI.Kadison.PreHilbert.wordMap_continuous line 72
  6. lemma OAI.Kadison.TracialGNS.conjugation_continuous line 86
  7. lemma OAI.Kadison.TracialGNS.centeredConjugation_continuous line 95
  8. lemma OAI.Kadison.TracialGNS.wordConjugation_continuous line 100
  9. lemma OAI.Kadison.TracialGNS.sumConjugation_continuous line 107
  10. lemma OAI.Kadison.TracialGNS.freeConjugation_continuous line 116