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 获取。