Compactness Under Constructive Scrutiny
Degree GrantorUniversity of Canterbury
Degree NameDoctor of Philosophy
The aim of this thesis is to understand the constructive scope of compactness. We show that it is possible to deﬁne, 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 deﬁne compactness constructively in a topological space. We investigate exactly what principles are necessary and suﬃcient to prove classically true theorems about compactness, as well as their antitheses. We develop beginnings of a constructive theory of diﬀerentiable manifolds.