coe_toStarSubalgebra

Mathlib.Analysis.VonNeumannAlgebra.Basic

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

English

The coercion of the star-subalgebra associated to S to a set equals S itself.

Русский

Приведение к множеству звёзд-подалгебры, связанной с S, даёт S в точности.

LaTeX

$$$(S.toStarSubalgebra : Set (H \\to L_{\\mathbb{C}} H)) = S$$$

Lean4

@[simp]
theorem coe_toStarSubalgebra (S : VonNeumannAlgebra H) : (S.toStarSubalgebra : Set (H →L[ℂ] H)) = S :=
  rfl

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

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

Разделы

Аффилиация

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