English
If the image of m in R[M] lies in the span of the closure of images of S, then m lies in the closure of S (via corresponding identifications).
Русский
Если образ m в R[M] лежит в линейной оболочке замыкания образов S, то m лежит в замыкании S.
LaTeX
$$$\\text{mem}_{R}(\\,\\mathrm{of}'_R M m,\\; \\operatorname{span}_R(\\operatorname{Submonoid}.closure(\\mathrm{of}'_R M'' S))) \\Rightarrow m \\in \\operatorname{closure} S$$$
Lean4
/-- If the image of an element `m : M` in `R[M]` belongs the submodule generated by
the closure of some `S : Set M` then `m ∈ closure S`. -/
theorem mem_closure_of_mem_span_closure [Nontrivial R] {m : M} {S : Set M}
(h : of' R M m ∈ span R (Submonoid.closure (of' R M '' S) : Set R[M])) : m ∈ closure S :=
by
suffices Multiplicative.ofAdd m ∈ Submonoid.closure (Multiplicative.toAdd ⁻¹' S) by simpa [← toSubmonoid_closure]
let S' := @Submonoid.closure (Multiplicative M) Multiplicative.mulOneClass S
have h' : Submonoid.map (of R M) S' = Submonoid.closure ((fun x : M => (of R M) x) '' S) := MonoidHom.map_mclosure _ _
rw [Set.image_congr' (show ∀ x, of' R M x = of R M x from fun x => of'_eq_of x), ← h'] at h
simpa using of'_mem_span.1 h
