OAI/Analysis/KadisonSimilarity/Representation/VectorL2Representation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual unital star representation of continuous scalar functions on the vector-valued L² space.

  1. theorem OAI.KadisonSimilarity.VectorL2.continuousL2Mul_star line 18
  2. def OAI.KadisonSimilarity.VectorL2.continuousRepresentation line 28