English
Any Cauchy sequence f in Padic p converges in the p-adic numbers: there exists q ∈ ℚ_p such that for every ε>0 there is N with |f(i) - q|_p < ε for all i ≥ N.
Русский
Любая последовательность Коши f в p-адических числах сходится в ℚ_p: существует q ∈ ℚ_p such that для любого ε>0 найдётся N с |f(i) - q|_p < ε для всех i ≥ N.
LaTeX
$$$\exists q \in \mathbb{Q}_p\;\forall ε>0\;\exists N\;\forall i\ge N:\; |f(i) - q|_p < ε$$$
Lean4
theorem complete' : ∃ q : ℚ_[p], ∀ ε > 0, ∃ N, ∀ i ≥ N, padicNormE (q - f i : ℚ_[p]) < ε :=
⟨lim f, fun ε hε ↦ by
obtain ⟨N, hN⟩ := exi_rat_seq_conv f (half_pos hε)
obtain ⟨N2, hN2⟩ := padicNormE.defn (lim' f) (half_pos hε)
refine ⟨max N N2, fun i hi ↦ ?_⟩
rw [← sub_add_sub_cancel _ (lim' f i : ℚ_[p]) _]
refine (padicNormE.add_le _ _).trans_lt ?_
rw [← add_halves ε]
apply _root_.add_lt_add
· apply hN2 _ (le_of_max_le_right hi)
· rw [padicNormE.map_sub]
exact hN _ (le_of_max_le_left hi)⟩
