isPrecomplete_iff — Mathlib

English

IsPrecomplete I M is equivalent to the property that every Cauchy sequence modulo powers has a limit modulo those powers.

Русский

IsPrecomplete I M эквивалентно свойству: любая последовательность, сходящаяся модульно по степеням I, имеет предел modulo этих степеней.

LaTeX

$$$IsPrecomplete\ I\ M \iff \forall f:\\mathbb{N} \to M,\ (\forall m,n, m \le n \Rightarrow f_m \equiv f_n \pmod{I^m}) \Rightarrow \exists L, \forall n, f_n \equiv L \pmod{I^n}$$$

Lean4

theorem isPrecomplete_iff :
    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)] :=
  ⟨fun h => h.1, fun h => ⟨h⟩⟩

Похожие утверждения