English
The rational-valued sequence limSeq f is Cauchy with respect to the p-adic metric: for every ε>0 there exists N such that for all i,j ≥ N, |limSeq f(i) - limSeq f(j)|_p < ε.
Русский
Кошьевая последовательность рационалов limSeq f удовлетворяет критерию Коши в p-адической метрике: для каждого ε>0 существует N, что для всех i,j ≥ N дистанция |limSeq f(i) − limSeq f(j)|_p < ε.
LaTeX
$$$\forall ε>0\;\exists N\;\forall i,j \ge N:\; |(\limSeq f(i) - \limSeq f(j))|_p < ε$$$
Lean4
theorem exi_rat_seq_conv_cauchy : IsCauSeq (padicNorm p) (limSeq f) := fun ε hε ↦
by
have hε3 : 0 < ε / 3 := div_pos hε (by simp)
let ⟨N, hN⟩ := exi_rat_seq_conv f hε3
let ⟨N2, hN2⟩ := f.cauchy₂ hε3
exists max N N2
intro j hj
suffices padicNormE (limSeq f j - f (max N N2) + (f (max N N2) - limSeq f (max N N2)) : ℚ_[p]) < ε
by
ring_nf at this
rw [← padicNormE.eq_padic_norm']
exact mod_cast this
apply lt_of_le_of_lt
· apply padicNormE.add_le
· rw [← add_thirds ε]
apply _root_.add_lt_add
· suffices padicNormE (limSeq f j - f j + (f j - f (max N N2)) : ℚ_[p]) < ε / 3 + ε / 3 by
simpa only [sub_add_sub_cancel]
apply lt_of_le_of_lt
· apply padicNormE.add_le
· apply _root_.add_lt_add
· rw [padicNormE.map_sub]
apply mod_cast hN j
exact le_of_max_le_left hj
· exact hN2 _ (le_of_max_le_right hj) _ (le_max_right _ _)
· apply mod_cast hN (max N N2)
apply le_max_left
