Theorems · Definition · functional analysis

VonNeumannAlgebra.toStarSubalgebra

{H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [inst_2 : CompleteSpace H] → VonNeumannAlgebra H → StarSubalgebra ℂ (H →L[ℂ] H)

Consider a von Neumann algebra acting on a Hilbert space H as a \*-subalgebra of H →L[ℂ] H. (That is, we forget that it is equal to its double commutant or equivalently that it is closed in the weak and strong operator topologies.)

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

3 results in Mathlib

Foundations

Depth 196 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace