English
Let s be a subset of M. The submodule span_R(s) is finitely generated if and only if there exists a finite subset s' of s such that span_R(s) = span_R(s').
Русский
Пусть s ⊆ M. Подмодуль Span_R(s) конечнопорожден тогда и только тогда, когда существует конечное подмножество s' ⊆ s такое, что span_R(s) = span_R(s').
LaTeX
$$$\operatorname{span}_R(s).FG \\iff \\exists s' : Finset M, (↑s' \subseteq s) \land \operatorname{span}_R(s) = \operatorname{span}_R(s')$$$
Lean4
theorem fg_span_iff_fg_span_finset_subset (s : Set M) :
(span R s).FG ↔ ∃ s' : Finset M, ↑s' ⊆ s ∧ span R s = span R s' :=
by
unfold FG
constructor
· intro ⟨s'', hs''⟩
obtain ⟨s', hs's, hss'⟩ := subset_span_finite_of_subset_span <| hs'' ▸ subset_span
refine ⟨s', hs's, ?_⟩
apply le_antisymm
· rwa [← hs'', Submodule.span_le]
· rw [Submodule.span_le]
exact le_trans hs's subset_span
· intro ⟨s', _, h⟩
exact ⟨s', h.symm⟩
