English
For a Cauchy sequence f of p-adic numbers, the limSeq f is a sequence of rationals that has the same limit point as f in the p-adic metric.
Русский
Для последовательности Коши f в p-адических числах limSeq f является последовательностью рациональных чисел, имеющей ту же предельную точку, что и f в метрике p-адических чисел.
LaTeX
$$$\text{Let } f:\ CauSeq(\mathbb{Q}_p, |\cdot|_p) \Rightarrow \lim f \in \mathbb{Q}_p.\ \text{There exists } (q_n)_{n\in\mathbb{N}} \subset \mathbb{Q} \text{ with } q_n \to \lim f \text{ in } \mathbb{Q}_p.$$$
Lean4
/-- `limSeq f`, for `f` a Cauchy sequence of `p`-adic numbers, is a sequence of rationals with the
same limit point as `f`. -/
def limSeq : ℕ → ℚ := fun n ↦ Classical.choose (rat_dense' (f n) (div_nat_pos n))
