toNonUnitalSubalgebra_toNonUnitalStarSubalgebra

English

A star-structure on a nonunital subalgebra induces the original star-subalgebra.

Русский

Звёздовая структура на неединичной подалгебре порождает исходную звёздную подпалгебру.

LaTeX

$$toNonUnitalStarSubalgebra(h_star)(s)(star_mem) = s$$

Lean4

@[simp]
theorem _root_.NonUnitalStarSubalgebra.toNonUnitalSubalgebra_toNonUnitalStarSubalgebra
    (S : NonUnitalStarSubalgebra R A) :
    (S.toNonUnitalSubalgebra.toNonUnitalStarSubalgebra fun _ => star_mem (s := S)) = S :=
  SetLike.coe_injective rfl

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