instNonUnitalCommCStarAlgebraSubtypeMemNonUnitalStarSubalgebraComplexElementalOfIsStarNormal

English

If S is a closed star-subalgebra of a commutative C*-algebra A, then S is a commutative C*-algebra.

Русский

Если S — замкнутая звезд-подалгебра коммутативной C*-алгебры A, то S является коммутативной C*-алгеброй.

LaTeX

$$$CommCStarAlgebra(A) \wedge IsClosed(S) \Rightarrow CommCStarAlgebra(S)$$$

Lean4

noncomputable instance [NonUnitalCStarAlgebra A] (x : A) [IsStarNormal x] :
    NonUnitalCommCStarAlgebra (NonUnitalStarAlgebra.elemental ℂ x) where

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