denseRange_ratCast — Mathlib

English

A variant form of Padic completeness: there exists q ∈ ℚ_p such that f(i) → q in the p-adic metric.

Русский

Вариант полноты: существует q ∈ ℚ_p такой, что f(i) сходится к q в p-адической метрике.

LaTeX

$$$\exists q \in \mathbb{Q}_p\;\forall ε>0:\; \exists N:\; \forall i\ge N:\; |f(i) - q|_p < ε$$$

Lean4

theorem denseRange_ratCast : DenseRange ((↑) : ℚ → ℚ_[p]) :=
  by
  intro x
  rw [Metric.mem_closure_range_iff]
  exact fun _ ↦ Padic.rat_dense _ x

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