map_toNonUnitalSubalgebra — Mathlib

English

The underlying nonunital subalgebra of the image map f S equals the image under f of the underlying nonunital subalgebra S.

Русский

Подлежащая неединичная подпалгебра образа map f S равна образу f исходной неединичной подпалгебры S.

LaTeX

$$(map f S).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra.$$

Lean4

theorem map_toNonUnitalSubalgebra {S : NonUnitalStarSubalgebra R A} {f : F} :
    (map f S : NonUnitalStarSubalgebra R B).toNonUnitalSubalgebra = NonUnitalSubalgebra.map f S.toNonUnitalSubalgebra :=
  SetLike.coe_injective rfl

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