Ultrametric Structure for Restriction Spaces

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.