English
The embedding of rationals into the p-adic numbers is injective (cast form).
Русский
Встраивание рациональных чисел в p-адические числа инъективно (в форме приведения).
LaTeX
$$$\\uparrow q = \\uparrow r \\iff q=r$$$
Lean4
theorem defn (f : PadicSeq p) {ε : ℚ} (hε : 0 < ε) : ∃ N, ∀ i ≥ N, padicNormE (Padic.mk f - f i : ℚ_[p]) < ε :=
by
dsimp [padicNormE]
-- `change ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε` also works, but is very slow
suffices hyp : ∃ N, ∀ i ≥ N, (f - const _ (f i)).norm < ε by peel hyp with N; use N
by_contra! h
obtain ⟨N, hN⟩ := cauchy₂ f hε
rcases h N with ⟨i, hi, hge⟩
have hne : ¬f - const (padicNorm p) (f i) ≈ 0 := fun h ↦
by
rw [PadicSeq.norm, dif_pos h] at hge
exact not_lt_of_ge hge hε
unfold PadicSeq.norm at hge; split_ifs at hge
apply not_le_of_gt _ hge
cases _root_.le_total N (stationaryPoint hne) with
| inl hgen => exact hN _ hgen _ hi
| inr hngen =>
have := stationaryPoint_spec hne le_rfl hngen
rw [← this]
exact hN _ le_rfl _ hi
