English
Let S be a subalgebra of A equipped with a star-closure property h turning it into a star-subalgebra. Then the underlying carrier set of the star-subalgebra ⟨S, h⟩ is exactly S.
Русский
Пусть S — подалгебра A, снабжённая свойством замкнутости относительно звездной операции h, превращающим его в звездную подалгебру. Тогда носитель звездной подалгебры ⟨S, h⟩ равен S.
LaTeX
$$$\bigl(\langle S, h\rangle : \text{StarSubalgebra} \; R \; A\bigr)\,\text{carrier} = S$$$
Lean4
@[simp]
theorem coe_mk (S : Subalgebra R A) (h) : ((⟨S, h⟩ : StarSubalgebra R A) : Set A) = S :=
rfl