adjoin_le_starAlgebra_adjoin — Mathlib

English

For any subset s of A, the nonunital star-subalgebra generated by s is contained in the nonunital star-subalgebra underlying the star-subalgebra generated by s.

Русский

Для произвольного подмножества s подалгебры A, порожденное немонолитной звездной субалгеброй, входит в соответствующую безединичную звездную подалгебру.

LaTeX

$$$ \operatorname{adjoin}_R s \le (\operatorname{StarAlgebra.adjoin}_R s).toNonUnitalStarSubalgebra $$$

Lean4

theorem adjoin_le_starAlgebra_adjoin (s : Set A) : adjoin R s ≤ (StarAlgebra.adjoin R s).toNonUnitalStarSubalgebra :=
  adjoin_le <| StarAlgebra.subset_adjoin R s

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