English
If a finite set t ⊆ Span_R(S) is contained in Submodule.span R s, then there exists T ⊆ S finite such that t ⊆ Span_R(T).
Русский
Если конечное множество t ⊆ Span_R(S) содержится в Submodule.span R s, то существует конечное T ⊆ S такое, что t ⊆ Span_R(T).
LaTeX
$$ht : (t : Finset M) ⊆ span R s → ∃ T : Finset M, ↑T ⊆ s ∧ (t : Set M) ⊆ span R (T : Set M)$$
Lean4
theorem subset_span_finite_of_subset_span {s : Set M} {t : Finset M} (ht : (t : Set M) ⊆ span R s) :
∃ T : Finset M, ↑T ⊆ s ∧ (t : Set M) ⊆ span R (T : Set M) := by
classical
induction t using Finset.induction_on with
| empty => exact ⟨∅, by simp⟩
| insert a t hat IH =>
obtain ⟨T, hTs, htT⟩ := IH (by simp_all [Set.insert_subset_iff])
obtain ⟨T', hT's, haT'⟩ := mem_span_finite_of_mem_span (ht (Finset.mem_insert_self _ _))
refine ⟨T ∪ T', by simp_all, ?_⟩
simp only [Finset.coe_insert, Finset.coe_union, span_union, insert_subset_iff, SetLike.mem_coe]
exact ⟨mem_sup_right haT', htT.trans (le_sup_left (a := span R _))⟩
