English
A variant expressing span membership via a finite linear combination indexed by a finite set.
Русский
Вариант выражения принадлежности span через конечную линейную комбинацию, индексируемую конечным множеством.
LaTeX
$$$m \in \operatorname{span}_R s \iff \exists n, \exists f:\mathrm{Fin}\,n \to R, \exists g:\mathrm{Fin}\,n \to s, \sum_{i=0}^{n-1} f(i) \cdot g(i) = 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 a sum indexed by `Fin n` for some `n`. -/
theorem mem_span_set' {m : M} {s : Set M} :
m ∈ Submodule.span R s ↔ ∃ (n : ℕ) (f : Fin n → R) (g : Fin n → s), ∑ i, f i • (g i : M) = m :=
by
refine ⟨fun h ↦ ?_, ?_⟩
· rcases mem_span_set.1 h with ⟨c, cs, rfl⟩
have A : c.support ≃ Fin c.support.card := Finset.equivFin _
refine ⟨_, fun i ↦ c (A.symm i), fun i ↦ ⟨A.symm i, cs (A.symm i).2⟩, ?_⟩
rw [Finsupp.sum, ← Finset.sum_coe_sort c.support]
exact Fintype.sum_equiv A.symm _ (fun j ↦ c j • (j : M)) (fun i ↦ rfl)
· rintro ⟨n, f, g, rfl⟩
exact Submodule.sum_mem _ (fun i _ ↦ Submodule.smul_mem _ _ (Submodule.subset_span (g i).2))
