In this article, we present a formalization of spherically complete spaces, which is a fundamental notion in non-archimedean functional analysis. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples and non-examples such as the field $\mathbf{C}_p$ of $p$-adic complex numbers. As applications, we formalize the Birkhoff-James orthogonality, Hahn-Banach extension theorem and the spherical completion for non-archimedean Banach spaces. Code available at https://github.com/YijunYuan/SphericalCompleteness

翻译：本文提出了球完备空间的形式化，这是非阿基米德泛函分析中的一个基本概念。这项工作包括球完备空间的等价定义、其基本性质、示例及反例（例如$p$进复数域$\mathbf{C}_p$）。作为应用，我们形式化了非阿基米德巴拿赫空间中的Birkhoff-James正交性、Hahn-Banach延拓定理以及球完备化过程。代码发布于https://github.com/YijunYuan/SphericalCompleteness