Refine search
Actions for selected content:
1 results
FORMALIZATION OF NON-ARCHIMEDEAN FUNCTIONAL ANALYSIS 1: SPHERICALLY COMPLETE SPACES
- Part of
-
- Journal:
- The Journal of Symbolic Logic , First View
- Published online by Cambridge University Press:
- 21 October 2026, pp. 1-31
-
- Article
-
- You have access
- HTML
- Export citation
-
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 $\textbf {C}_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.
