adjoin_eq_starClosure_adjoin — Mathlib

English

For any subset s of A, the adjoin of s is equal to the star-closure of the nonunital algebra generated by s.

Русский

Для множества s ⊆ A адъюнтация R s равна звездной замкнутости ненулевой алгебры, порожденной s.

LaTeX

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

Lean4

theorem adjoin_eq_starClosure_adjoin (s : Set A) : adjoin R s = (NonUnitalAlgebra.adjoin R s).starClosure :=
  toNonUnitalSubalgebra_injective <|
    show NonUnitalAlgebra.adjoin R (s ∪ star s) = NonUnitalAlgebra.adjoin R s ⊔ star (NonUnitalAlgebra.adjoin R s) from
      (NonUnitalSubalgebra.star_adjoin_comm R s).symm ▸ NonUnitalAlgebra.adjoin_union s (star s)

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