English
If M' is finitely generated and iSup N is used to approximate M' along a chain N, then there exists a finite stage n with M' = N(n).
Русский
Если M' конечно порожден и iSup N приближает M' по цепочке, то существует конечный этап n, при котором M' = N(n).
LaTeX
$$∃ n, M' = N(n) given hM' and H: iSup N = M'$$
Lean4
theorem stabilizes_of_iSup_eq {M' : Submodule R M} (hM' : M'.FG) (N : ℕ →o Submodule R M) (H : iSup N = M') :
∃ n, M' = N n := by
obtain ⟨S, hS⟩ := hM'
have : ∀ s : S, ∃ n, (s : M) ∈ N n := fun s =>
(Submodule.mem_iSup_of_chain N s).mp
(by
rw [H, ← hS]
exact Submodule.subset_span s.2)
choose f hf using this
use S.attach.sup f
apply le_antisymm
· conv_lhs => rw [← hS]
rw [Submodule.span_le]
intro s hs
exact N.2 (Finset.le_sup <| S.mem_attach ⟨s, hs⟩) (hf _)
· rw [← H]
exact le_iSup _ _
