nonUnitalCommCStarAlgebra — Mathlib

English

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

Русский

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

LaTeX

$$$NonUnitalCommCStarAlgebra(A) \wedge S \subseteq A \wedge IsClosed(S) \Rightarrow NonUnitalCommCStarAlgebra(S)$$$

Lean4

instance nonUnitalCommCStarAlgebra {S A : Type*} [NonUnitalCommCStarAlgebra A] [SetLike S A] [NonUnitalSubringClass S A]
    [SMulMemClass S ℂ A] [StarMemClass S A] (s : S) [h_closed : IsClosed (s : Set A)] : NonUnitalCommCStarAlgebra 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 _ _

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