English
The rational numbers are dense in the p-adic numbers: for every p-adic number q and every positive rational ε, there exists a rational r with the p-adic distance |q − r|₂p less than ε.
Русский
Рациональные числа плотно заполнены в p-адических числах: для каждого p-адического числа q и любого положительного рационального ε существует рациональное число r такое, что p-адическая дистанция |q − r|ₚ < ε.
LaTeX
$$$\forall q \in \mathbb{Q}_p\;\forall \varepsilon \in \mathbb{Q}_{>0}:\ \exists r \in \mathbb{Q}: |q - r|_p < \varepsilon$$$
Lean4
theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicNormE (q - r : ℚ_[p]) < ε :=
Quotient.inductionOn q fun q' ↦
have : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (q' m - q' n) < ε := cauchy₂ _ hε
let ⟨N, hN⟩ := this
⟨q' N, by
classical
dsimp [padicNormE]
convert_to PadicSeq.norm (q' - const _ (q' N)) < ε
rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
· simpa only [heq, PadicSeq.norm, dif_pos]
· simp only [PadicSeq.norm, dif_neg hne']
change padicNorm p (q' _ - q' _) < ε
rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
· have := (stationaryPoint_spec hne' le_rfl hle).symm
simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
simpa only [this]
· exact hN _ (lt_of_not_ge hle).le _ le_rfl⟩
