# 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

The set of p-adic integers `ℤ_[p]`

is totally bounded.

The set of p-adic integers `ℤ_[p]`

is a compact topological space.

## Equations

- ⋯ = ⋯

The field of p-adic numbers `ℚ_[p]`

is a proper metric space.

## Equations

- ⋯ = ⋯