English
For any subalgebra S of A over R, the underlying set of its star-closure equals the underlying set of the join S ⊔ star S. In other words, the elements of the star-closure are exactly those that belong to the join of S with its star.
Русский
Для любой подалгебры S в A над R множество элементов звёздного замыкания совпадает с множеством элементов объединения S и S^{*}. Другими словами, элементы звёздного замыкания равны тем, что принадлежат объединению S и Star(S).
LaTeX
$$$(\mathrm{StarClosure}(S)) = S \sqcup S^{*}$ as sets, i.e. \{a : A : a ∈ \mathrm{StarClosure}(S)\} = \{a : A : a ∈ S \lor a ∈ S^{*}\}.$$$
Lean4
@[simp]
theorem coe_starClosure (S : Subalgebra R A) : (S.starClosure : Set A) = (S ⊔ star S : Subalgebra R A) :=
rfl
