theorem Submodule.subset_finite_subset_subset_span (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (t : Finset M) (ht : ↑t ⊆ ↑(span R s)) : ∃ (s' : Finset M), ↑s' ⊆ s ∧ ↑t ⊆ ↑(span R ↑s')

theorem Submodule.fg_span_iff_fg_span_finset_subset (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : (span R s).FG ↔ ∃ (s' : Finset M), ↑s' ⊆ s ∧ span R s = span R ↑s'