English
The field of p-adic numbers ℚ_[p] is a proper metric space.
Русский
Поле p-адических чисел ℚ_p является правильным метрическим пространством.
LaTeX
$$$\\\\text{ProperSpace }\\\\mathbb{Q}_{p}$$$
Lean4
/-- The field of p-adic numbers `ℚ_[p]` is a proper metric space. -/
instance : ProperSpace ℚ_[p] :=
by
suffices LocallyCompactSpace ℚ_[p] from .of_nontriviallyNormedField_of_weaklyLocallyCompactSpace _
have : closedBall 0 1 ∈ 𝓝 (0 : ℚ_[p]) := closedBall_mem_nhds _ zero_lt_one
simp only [closedBall, dist_eq_norm_sub, sub_zero] at this
refine IsCompact.locallyCompactSpace_of_mem_nhds_of_addGroup ?_ this
simpa only [isCompact_iff_compactSpace] using PadicInt.compactSpace p