DOI: 10.1017/jsl.2026.10251 ISSN: 0022-4812

FORMALIZATION OF NON-ARCHIMEDEAN FUNCTIONAL ANALYSIS 1: SPHERICALLY COMPLETE SPACES

YIJUN YUAN
Show PDF Cite

Abstract

In this article, we present a formalization of spherically complete spaces, a fundamental notion in non-Archimedean functional analysis, using the Lean theorem prover (v4.31.0), building over Mathlib. This work includes the equivalent definitions of spherically complete spaces, their basic properties, examples, and non-examples such as the field

C p $\textbf {C}_p$ bold upper C Subscript p
of p -adic complex numbers. As applications, we formalize the notion of Birkhoff–James orthogonality, the Hahn–Banach extension theorem and the spherical completion for non-Archimedean Banach spaces.

More from our Archive