English
The set of all p-adic integers is totally bounded.
Русский
Множество всех p-адических целых чисел totally bounded.
LaTeX
$$\\(\\\\text{TotallyBounded}( \\text{Set.univ} : \\text{Set } \\mathbb{Z}_{p})\\)$$
Lean4
/-- The set of p-adic integers `ℤ_[p]` is totally bounded. -/
theorem totallyBounded_univ : TotallyBounded (Set.univ : Set ℤ_[p]) :=
by
refine Metric.totallyBounded_iff.mpr (fun ε hε ↦ ?_)
obtain ⟨k, hk⟩ := exists_pow_neg_lt p hε
refine ⟨Nat.cast '' Finset.range (p ^ k), Set.toFinite _, fun z _ ↦ ?_⟩
simp only [PadicInt, Set.mem_iUnion, Metric.mem_ball, exists_prop, Set.exists_mem_image]
refine ⟨z.appr k, ?_, ?_⟩
· simpa only [Finset.mem_coe, Finset.mem_range] using z.appr_lt k
· exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk
