Theorems · Theorem · functional analysis

VonNeumannAlgebra.mk.inj

∀ {H : Type u} {inst : NormedAddCommGroup H} {inst_1 : InnerProductSpace ℂ H} {inst_2 : CompleteSpace H}
  {toStarSubalgebra : StarSubalgebra ℂ (H →L[ℂ] H)}
  {centralizer_centralizer' : toStarSubalgebra.carrier.centralizer.centralizer = toStarSubalgebra.carrier}
  {toStarSubalgebra_1 : StarSubalgebra ℂ (H →L[ℂ] H)}
  {centralizer_centralizer'_1 : toStarSubalgebra_1.carrier.centralizer.centralizer = toStarSubalgebra_1.carrier},
  { toStarSubalgebra := toStarSubalgebra, centralizer_centralizer' := centralizer_centralizer' } =
      { toStarSubalgebra := toStarSubalgebra_1, centralizer_centralizer' := centralizer_centralizer'_1 } →
    toStarSubalgebra = toStarSubalgebra_1

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

1 results in Mathlib

Foundations

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