English
If x ∈ span_R S, then there exists a finite subset T ⊆ S such that x ∈ span_R(T).
Русский
Если x принадлежит span_R S, то существует конечное множество T ⊆ S такое, что x ∈ span_R(T).
LaTeX
$$∃ T : Finset M, ↑T ⊆ S ∧ x ∈ span_R (T : Set M)$$
Lean4
/-- For every element in the span of a set, there exists a finite subset of the set
such that the element is contained in the span of the subset. -/
theorem mem_span_finite_of_mem_span {S : Set M} {x : M} (hx : x ∈ span R S) :
∃ T : Finset M, ↑T ⊆ S ∧ x ∈ span R (T : Set M) := by
classical
refine span_induction (fun x hx => ?_) ?_ ?_ ?_ hx
· refine ⟨{ x }, ?_, ?_⟩
· rwa [Finset.coe_singleton, Set.singleton_subset_iff]
· rw [Finset.coe_singleton]
exact Submodule.mem_span_singleton_self x
· use ∅
simp
· rintro x y - - ⟨X, hX, hxX⟩ ⟨Y, hY, hyY⟩
refine ⟨X ∪ Y, ?_, ?_⟩
· rw [Finset.coe_union]
exact Set.union_subset hX hY
rw [Finset.coe_union, span_union, mem_sup]
exact ⟨x, hxX, y, hyY, rfl⟩
· rintro a x - ⟨T, hT, h2⟩
exact ⟨T, hT, smul_mem _ _ h2⟩
