English
There exists a finite-valued function f from a finite index set into M such that every image lies in s, span of the image equals span of s, and f is linearly independent as a family.
Русский
Существует конечнозначная функция f: Finite → M such that каждое значение f(i) ⊆ s, span( range f ) = span(s) и семейство f линейно независимо.
LaTeX
$$$\\exists f : Fin (\\operatorname{finrank}_K(\\operatorname{span}_K s)) \\to M, \\; (\\forall i, f(i) \\in s) \\land \\operatorname{span}_K(\\operatorname{range} f) = \\operatorname{span}_K s \\land \\operatorname{LinearIndependent} K f$$$
Lean4
/-- This is a version of `mem_span_set` with an estimate on the number of terms in the sum. -/
theorem mem_span_set_iff_exists_finsupp_le_finrank :
x ∈ span K s ↔
∃ c : M →₀ K, c.support.card ≤ finrank K (span K s) ∧ ↑c.support ⊆ s ∧ c.sum (fun mi r ↦ r • mi) = x :=
by
constructor
· intro h
rcases exists_finset_span_eq_linearIndepOn K s with ⟨t, ht_sub, ht_card, ht_span, ht_indep⟩
rcases mem_span_set.mp (ht_span ▸ h) with ⟨c, hct, hx⟩
refine ⟨c, ?_, hct.trans ht_sub, hx⟩
exact ht_card ▸ Finset.card_mono hct
· rintro ⟨c, -, hcs, hx⟩
exact mem_span_set.mpr ⟨c, hcs, hx⟩
