OAI/Analysis/KadisonKastler/SelfAdjointVectorSpace.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The closed real space of self-adjoint algebra vectors

  1. def OAI.KadisonKastler.selfAdjointVectorMap line 16
  2. def OAI.KadisonKastler.selfAdjointVectorSpace line 22
  3. instance OAI.KadisonKastler.selfAdjointVectorSpace_complete line 25
  4. def OAI.KadisonKastler.selfAdjointVectorInSpace line 29
  5. theorem OAI.KadisonKastler.selfAdjointVectorInSpace_dense line 33
  6. theorem OAI.KadisonKastler.inner_selfAdjointVector_projection line 42