mem_closure_image_of — Mathlib

English

If f is a ring homomorphism, then the image of the closure of s equals the closure of the image of s.

Русский

Если f — гомоморфизм колец, образ замыкания s равен замыканию образа s.

LaTeX

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

Lean4

theorem mem_closure_image_of (f : R →+* S) {s : Set R} {x : R} (hx : x ∈ Subring.closure s) :
    f x ∈ Subring.closure (f '' s) := by
  rw [← f.map_closure, Subring.mem_map]
  exact ⟨x, hx, rfl⟩

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