commutant_commutant

Mathlib.Analysis.VonNeumannAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#VonNeumannAlgebra.commutant_commutant

English

Reiterating, the double commutant of S equals S: S'' = S.

Русский

Снова: двойной коммутант S равен S: S'' = S.

LaTeX

$$$S^{\\prime\\prime} = S$$$

Lean4

@[simp]
theorem commutant_commutant (S : VonNeumannAlgebra H) : S.commutant.commutant = S :=
  SetLike.coe_injective <| by simp

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru