coe_mk — Mathlib

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

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