Theorems · Definition · functional analysis

VonNeumannAlgebra.casesOn

{H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] →
      [inst_2 : CompleteSpace H] →
        {motive : VonNeumannAlgebra H → Sort u_1} →
          (t : VonNeumannAlgebra H) →
            ((toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)) →
                (centralizer_centralizer' :
                    toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier) →
                  motive
                    { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' }) →
              motive t

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace