Abstract
In this entry, we explore the relationship
between restriction spaces and usual metric
structures by instantiating the former as ultrametric spaces.
This is classically captured by defining the distance as
$$\mathrm{dist} \ x \ y = \inf_{x \downarrow n \ = \ y \downarrow n} \left(\frac{1}{2}\right)^ n$$
but we actually generalize this perspective by introducing a hierarchy of increasingly
refined type classes to systematically relate ultrametric and restriction-based notions.
This layered approach enables a precise comparison of structural and topological properties.
In the end, our main result establishes that completeness in the sense of restriction spaces
coincides with standard metric completeness, thus bridging the gap between
our framework and Banach's fixed-point theorem established in HOL-Analysis.