English
An element x belongs to the span of a subset s of M iff there exist a finitely supported function f and a finite subset t of M such that t is contained in s, the support of f is contained in t, and x equals the finite sum ∑ a∈t f(a)·a.
Русский
Элемент x принадлежит span_R(s) тогда и только тогда, когда существуют конечноселек функция f и конечное подмножество t ⊆ s такие, что поддержка f ⊆ t и x = ∑_{a∈t} f(a)·a.
LaTeX
$$$x \in \operatorname{span}_R s \iff \exists f: M \to R, \exists t: \mathrm{Finset}\,M, \uparrow t \subseteq s \,\wedge\, \operatorname{support}(f) \subseteq t \wedge \sum_{a \in t} f(a) \cdot a = x$$$
Lean4
theorem mem_span_iff_exists_finset_subset {s : Set M} {x : M} :
x ∈ span R s ↔ ∃ (f : M → R) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∑ a ∈ t, f a • a = x
where
mp := by
rw [← s.image_id, mem_span_image_iff_linearCombination]
rintro ⟨l, hl, rfl⟩
exact ⟨l, l.support, by simpa [linearCombination, Finsupp.sum] using hl⟩
mpr := by rintro ⟨n, t, hts, -, rfl⟩; exact sum_mem fun x hx ↦ smul_mem _ _ <| subset_span <| hts hx
