Compactness Under Constructive Scrutiny
Hannes Diener · UC Research Repository (University of Canterbury) · 2008
The aim of this thesis is to understand the constructive scope of compactness. We show that it is possible to define, constructively, a meaningful notion of compactness in a more general setting than the uniform/metric space one. Furthermore, we show that it is not possible to define compactness constructively in a topological space. We investigate exactly what principles are necessary and sufficient to prove classically true theorems about compactness, as well as their antitheses. We develop beginnings of a constructive theory of differentiable manifolds.