mem_closure_of_mem_span_closure — Mathlib

English

If the image of m belongs to the span of the closure of S inside MonoidAlgebra, then m belongs to the closure of S.

Русский

Если образ m лежит в span(closure(S)) внутри MonoidAlgebra, тогда m ∈ closure(S).

LaTeX

$$$\\mathrm{mem}_{\\_} (\\mathrm{MonoidAlgebra}.of(m), \\mathrm{span}_R(\\mathrm{closure}(S))) \\Rightarrow m \\in \\mathrm{closure}(S)$$$

Lean4

/-- If the image of an element `m : M` in `MonoidAlgebra 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 (MonoidAlgebra R M))) : m ∈ closure S :=
  by
  rw [← MonoidHom.map_mclosure] at h
  simpa using of_mem_span_of_iff.1 h

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