map_adjoin — Mathlib

English

For a singleton {x}, the image under f of the subalgebra adjoin {x} equals adjoin {f x}.

Русский

Для единичного множества {x} образ отображения f образует подпалгебру, порожденную {f x}.

LaTeX

$$$\\operatorname{map} f (\\operatorname{adjoin} R \\{x\\}) = \\operatorname{adjoin} R \\{f x\\}$$$

Lean4

theorem _root_.NonUnitalStarAlgHom.map_adjoin (f : F) (s : Set A) : map f (adjoin R s) = adjoin R (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) NonUnitalStarAlgebra.gi.gc NonUnitalStarAlgebra.gi.gc fun _t =>
    rfl

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