map_top — Mathlib

English

The image under f of the subalgebra generated by a set s equals the subalgebra generated by the image of s.

Русский

Образ отображения f под подпалгеброй, порожденной множеством s, равен подпалгебре, порожденной образом s.

LaTeX

$$$\\operatorname{map} f (\\operatorname{adjoin} R\, s) = \\operatorname{adjoin} R (f''s)$$$

Lean4

@[simp]
theorem map_top [IsScalarTower R A A] [SMulCommClass R A A] [StarModule R A] (f : F) :
    (⊤ : NonUnitalStarSubalgebra R A).map f = NonUnitalStarAlgHom.range f :=
  SetLike.coe_injective Set.image_univ

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