mem_carrier — Mathlib

English

Membership in a von Neumann algebra's star-subalgebra equals membership in the algebra regarded as a set.

Русский

Членство в star-подалгебре алгебры Вона эквивалентно членству в самой алгебре как в множестве.

LaTeX

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

Lean4

@[simp]
theorem mem_carrier {S : VonNeumannAlgebra H} {x : H →L[ℂ] H} : x ∈ S.toStarSubalgebra ↔ x ∈ (S : Set (H →L[ℂ] H)) :=
  Iff.rfl

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