English
An element m ∈ M lies in the submodule span_R s if and only if m can be written as a finite R-linear combination of elements of s.
Русский
Элемент m ∈ M принадлежит порожденному подмножество span_R s тогда и только тогда, когда m может быть записано как конечная линейная комбинация элементов s.
LaTeX
$$$m \in \operatorname{span}_R s \iff \exists c: M \to_0 R, (c\text{ с поддержкой в }s) \wedge \sum_{a\in s} c(a)\cdot a = m$$$
Lean4
/-- An element `m ∈ M` is contained in the `R`-submodule spanned by a set `s ⊆ M`, if and only if
`m` can be written as a finite `R`-linear combination of elements of `s`.
The implementation uses `Finsupp.sum`. -/
theorem mem_span_set {m : M} {s : Set M} :
m ∈ Submodule.span R s ↔ ∃ c : M →₀ R, (c.support : Set M) ⊆ s ∧ (c.sum fun mi r => r • mi) = m :=
by
conv_lhs => rw [← Set.image_id s]
exact Finsupp.mem_span_image_iff_linearCombination R (v := _root_.id (α := M))
