map_adjoin — Mathlib

English

A homomorphism maps the adjoin of a set to the adjoin of its image: map_f(adjoin_R s) = adjoin_R (f''s).

Русский

Гомоморфизм переводит adjoin R s в adjoin R (f '' s).

LaTeX

$$$\operatorname{map}_f(\operatorname{adjoin}_R(s)) = \operatorname{adjoin}_R(f''s)$$$

Lean4

theorem _root_.NonUnitalAlgHom.map_adjoin [IsScalarTower R B B] [SMulCommClass R B B] (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) NonUnitalAlgebra.gi.gc NonUnitalAlgebra.gi.gc fun _t => rfl

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