adjoin_nonUnitalStarSubalgebra — Mathlib

English

The star-algebra generated by s, when regarded as a nonunital star-subalgebra, coincides with the adjoin generated by s as a star-subalgebra.

Русский

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

LaTeX

$$$ \operatorname{adjoin}_R(\operatorname{NonUnitalStarAlgebra.adjoin}_R s) = \operatorname{adjoin}_R s $$$

Lean4

theorem adjoin_nonUnitalStarSubalgebra (s : Set A) : adjoin R (NonUnitalStarAlgebra.adjoin R s : Set A) = adjoin R s :=
  le_antisymm (adjoin_le <| NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin R s)
    (adjoin_le <| (NonUnitalStarAlgebra.subset_adjoin R s).trans <| subset_adjoin R _)

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