coe_star — Mathlib

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

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