adjoin_eq_starClosure_adjoin — Mathlib

English

The same relation as above holds in a different presentation: adjoin R s = (Algebra.adjoin R s).starClosure.

Русский

Та же связь в другой формулировке: adjoin R s = (Algebra.adjoin R s).starClosure.

LaTeX

$$$\operatorname{adjoin}_{{\text{StarAlg}}}(R,s) = (\operatorname{Algebra.adjoin}(R,s)).\text{starClosure}$$$

Lean4

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

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