English
If I is an ideal and IsPrecomplete I M holds, then from any sequence f: ℕ → M, which is Cauchy modulo I^m top, there exists a limit L ∈ M such that f n ≡ L modulo I^n top for all n.
Русский
Если IsPrecomplete I M выполняется, то для любой последовательности f: ℕ → M, которая сходится относительно степеней I, существует предел L ∈ M такой, что f n ≡ L по модулю I^n топ.
LaTeX
$$$IsPrecomplete\ I\ M \Rightarrow \forall f: \mathbb{N} \to M,\ (\forall m\le n, f_m \equiv f_n \pmod{I^m \top}) \Rightarrow \exists L, \forall n, f_n \equiv L \pmod{I^n \top}$$$
Lean4
theorem prec (_ : IsPrecomplete I M) {f : ℕ → M} :
(∀ {m n}, m ≤ n → f m ≡ f n [SMOD (I ^ m • ⊤ : Submodule R M)]) →
∃ L : M, ∀ n, f n ≡ L [SMOD (I ^ n • ⊤ : Submodule R M)] :=
IsPrecomplete.prec' _
