Constructive Urysohn Universal Metric Space

Davorin Lešnik (Institute for Mathematics, Physics and Mechanics, Slovenia)

Abstract: We construct the Urysohn metric space in constructive setting without choice principles. The Urysohn space is a complete separable metric space which contains an isometric copy of every separable metric space, and any isometric embedding into it from a finite subspace of a separable metric space extends to the whole domain.

Keywords: Urysohn universal space, constructive mathematics, metric space

Categories: G.0