starClosure_eq_adjoin — Mathlib

English

The starClosure of S equals the adjoin of S in the star-algebra sense; i.e., S.starClosure = adjoin R (S : Set A).

Русский

Звёздное замыкание S совпадает с адджойном S в звёздной алгебре.

LaTeX

$$$S^{\star-closure} = \mathrm{adjoin}(R, S)$$$

Lean4

theorem _root_.Subalgebra.starClosure_eq_adjoin (S : Subalgebra R A) : S.starClosure = adjoin R (S : Set A) :=
  le_antisymm (Subalgebra.starClosure_le_iff.2 <| subset_adjoin R (S : Set A))
    (adjoin_le (le_sup_left : S ≤ S ⊔ star S))

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