Theorems · Theorem · functional analysis

VonNeumannAlgebra.mk.congr_simp

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

Defined in

Mathlib.Analysis.VonNeumannAlgebra.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupInnerProductSpaceCompleteSpace