adjoin_nonUnitalSubalgebra — Mathlib

English

The subalgebra generated by the non-unital subalgebra generated by s is the same as the subalgebra generated by s: adjoin_R (NonUnitalAlgebra.adjoin_R s) = adjoin_R s.

Русский

Подалгебра, порожденная нелеприведенной подалгеброй, порожденной s, совпадает с подалгеброй, порожденной s: adjoin_R (NonUnitalAlgebra.adjoin_R s) = adjoin_R s.

LaTeX

$$$ \operatorname{adjoin}_{R} \bigl(\operatorname{NonUnitalAlgebra.adjoin}_{R} s\bigr) = \operatorname{adjoin}_{R} s $$$

Lean4

theorem adjoin_nonUnitalSubalgebra (s : Set A) : adjoin R (NonUnitalAlgebra.adjoin R s : Set A) = adjoin R s :=
  le_antisymm (adjoin_le <| NonUnitalAlgebra.adjoin_le_algebra_adjoin R s)
    (adjoin_le <| (NonUnitalAlgebra.subset_adjoin R).trans subset_adjoin)

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