English
When s is a finite set (as a Finset), membership in span_R s is equivalent to the existence of a finitely supported function f with support contained in s whose finite sum equals x.
Русский
Для финального множества s равносильно существованию функции с конечной поддержкой, поддержка которой ⊆ s, и сумма которой даёт x.
LaTeX
$$$x \in \operatorname{span}_R s \iff \exists f: M \to R, f\text{ support} \subseteq s \wedge \sum_{a\in s} f(a)\,a = x$$$
Lean4
theorem mem_span_finset {s : Finset M} {x : M} : x ∈ span R s ↔ ∃ f : M → R, f.support ⊆ s ∧ ∑ a ∈ s, f a • a = x
where
mp := by
rw [mem_span_iff_exists_finset_subset]
rintro ⟨f, t, hts, hf, rfl⟩
refine ⟨f, hf.trans hts, .symm <| Finset.sum_subset hts ?_⟩
simp +contextual [Function.support_subset_iff'.1 hf]
mpr := by rintro ⟨f, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hx
