Properness of the p-adic numbers

In this file, we prove that ℤ_[p] is totally bounded and compact, and that ℚ_[p] is proper.

Main results

• PadicInt.totallyBounded_univ : The set of p-adic integers ℤ_[p] is totally bounded.
• PadicInt.compactSpace : The set of p-adic integers ℤ_[p] is a compact topological space.
• Padic.instProperSpace : The field of p-adic numbers ℚ_[p] is a proper metric space.

Notation

• p : Is a natural prime.

References

Gouvêa, F. Q. (2020) p-adic Numbers An Introduction. 3rd edition. Cham, Springer International Publishing

theorem PadicInt.totallyBounded_univ (p : ℕ) [Fact (Nat.Prime p)] : TotallyBounded Set.univ

The set of p-adic integers ℤ_[p] is totally bounded.

instance PadicInt.compactSpace (p : ℕ) [Fact (Nat.Prime p)] : CompactSpace ℤ_[p]

The set of p-adic integers ℤ_[p] is a compact topological space.

instance Padic.instProperSpace (p : ℕ) [Fact (Nat.Prime p)] : ProperSpace ℚ_[p]

The field of p-adic numbers ℚ_[p] is a proper metric space.