OAI/Analysis/KadisonSimilarity/Representation/SeparableConcretePredual.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A separable concrete Hilbert space gives a separable Banach predual. Only the norm-continuity of vector coefficients and their defining density are used.

  1. def OAI.KadisonSimilarity.predualCoefficientBilinear line 15
  2. theorem OAI.KadisonSimilarity.predualCoefficient_continuous line 23
  3. theorem OAI.KadisonSimilarity.normalCoefficient_continuous line 29
  4. instance OAI.KadisonSimilarity.concretePredual_separable line 36

    Source documentation

    The vector predual has a countable norm-dense subset whenever the represented Hilbert space does.

    instance concretePredual_separable [TopologicalSpace.SeparableSpace H] :
    TopologicalSpace.SeparableSpace (ConcretePredual M) := by
…

    Mentions: OAI.KadisonSimilarity.ConcretePredual