Learn · Topology
Axeyum for topologists
Axeyum currently treats continuity and compact-interval arguments through explicit real analysis rather than through a general theory of spaces.
a103b3db3 Measured Source Axeyum fact ledger and implementation documentation After reading this guide, you should be able to
Learning objectives
- Identify the parts of Axeyum that are relevant to topology.
- Distinguish implemented results from the current research frontier.
- Open a lesson or artifact that provides the underlying definitions and evidence.
Current state
What topological ideas are already present in the analysis library?
The constructed-real library has continuity and uniform continuity on intervals, explicit moduli, interval suprema, bisection, and compact-interval approximation results. These are concrete topological phenomena with executable data attached.
The present interval results provide a tested body of examples for a general theory of metric and topological spaces. That abstraction is the next layer of the formal library.
Why it matters
What the current work makes possible
- Continuity hypotheses carry explicit information used by algorithms.
- The library formalizes where unrestricted completeness principles imply classical logic.
- Existing interval theorems can test whether a future abstraction preserves computational content.
Results to inspect
Open the evidence
What comes next
Extend the present base
The next step is a general metric-space and topological-space layer with open and closed sets, continuous maps, products, compactness, and connectedness.
A constructive treatment can then compare several forms of compactness and completeness instead of treating their classical equivalence as automatic.
Where to begin