Completion of premetric spaces

TL;DR

This paper introduces a method for completing premetric spaces within a constructive mathematics framework that does not rely on countable choice, expanding the tools available for such spaces.

Contribution

The paper proposes a novel completion method for premetric spaces compatible with constructive mathematics without countable choice.

Findings

Provides a constructive completion technique for premetric spaces.

Extends the theory of premetric spaces in constructive settings.

Facilitates further research in constructive analysis and topology.

Abstract

We present a method for completing a premetric space, in the sense introduced by F. Richman in the context of constructive Mathematics without countable choice.