Precompact Apartness Spaces

TL;DR

This paper introduces a constructive notion of precompactness for apartness spaces, expanding the understanding of their properties without relying on uniform structures, within a Bishop-style framework.

Contribution

It defines and studies precompactness in apartness spaces without uniformity, advancing constructive theories of apartness and uniformity.

Findings

Precompactness characterized in non-uniform apartness spaces

Properties of precompactness established constructively

Contributes to the development of constructive topology

Abstract

We present a notion of precompactness, and study some of its properties, in the context of apartness spaces whose apartness structure is not necessarily induced by any uniform one. The presentation lies entirely with a Bishop-style constructive framework, and is a contribution to the ongoing development of the constructive theories of apartness and uniformity.