map_closure — Mathlib

English

The image under a nonunital ring homomorphism f of the closure of a set s is equal to the closure of the image of s: closure(s) map f = closure(f''s).

Русский

Образ подгруппы closure s через отображение f совпадает с closure образа s: closure(s) map f = closure(f''s).

LaTeX

$$$\mathrm{closure}(s)\mapsto f = \mathrm{closure}(f''s)$$$

Lean4

/-- The image under a ring homomorphism of the `NonUnitalSubring` generated by a set equals
the `NonUnitalSubring` generated by the image of the set. -/
theorem map_closure (f : R →ₙ+* S) (s : Set R) : (closure s).map f = closure (f '' s) :=
  Set.image_preimage.l_comm_of_u_comm (gc_map_comap f) (NonUnitalSubring.gi S).gc (NonUnitalSubring.gi R).gc fun _ ↦ rfl

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