English
The underlying set of the star of a subalgebra coincides with the star of the underlying set of the subalgebra.
Русский
Функция перехода к множеству сохраняется под звездой: множество звезды подалгебры совпадает со звездой множества исходной подалгебры.
LaTeX
$$$$\big(\star S\big) \text{ as a set} = \star\big(S \text{ as a set}\big).$$$$
Lean4
@[simp]
theorem coe_star (S : Subalgebra R A) : ((star S : Subalgebra R A) : Set A) = star (S : Set A) :=
rfl