English
Let A be a commutative C*-algebra and S be a closed star-subalgebra of A. Then S, with the inherited operations, is a commutative C*-algebra.
Русский
Пусть A — коммутативная C*-алгебра, а S — замкнутая звезд-subалгебра A. Тогда S, с ограниченными операциями, является коммутативной C*-алгеброй.
LaTeX
$$$CommCStarAlgebra(A) \wedge S \subseteq A \wedge IsClosed(S) \Rightarrow CommCStarAlgebra(S)$$$
Lean4
instance commCStarAlgebra {S A : Type*} [CommCStarAlgebra A] [SetLike S A] [SubringClass S A] [SMulMemClass S ℂ A]
[StarMemClass S A] (s : S) [h_closed : IsClosed (s : Set A)] : CommCStarAlgebra s
where
toCompleteSpace := h_closed.completeSpace_coe
norm_mul_self_le x := CStarRing.norm_star_mul_self (x := (x : A)) |>.symm.le
mul_comm _ _ := Subtype.ext <| mul_comm _ _
