complete — Mathlib

English

The p-adic integers Z_p are complete with respect to the norm, i.e., every Cauchy sequence converges in Z_p.

Русский

p-адические целые Z_p являются полными по норме: всякая последовательность Коши сходится в Z_p.

LaTeX

$$$$\text{CauSeq.IsComplete}(\mathbb{Z}_p, \|\cdot\|).$$$$

Lean4

instance complete : CauSeq.IsComplete ℤ_[p] norm :=
  ⟨fun f =>
    have hqn : ‖CauSeq.lim (cauSeq_to_rat_cauSeq f)‖ ≤ 1 := padicNormE_lim_le zero_lt_one fun _ => norm_le_one _
    ⟨⟨_, hqn⟩, fun ε => by simpa [norm, norm_def] using CauSeq.equiv_lim (cauSeq_to_rat_cauSeq f) ε⟩⟩

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