JUCS - Journal of Universal Computer Science 15(6): 1236-1263, doi: 10.3217/jucs-015-06-1236
Constructive Urysohn Universal Metric Space
expand article infoDavorin Lešnik‡
‡ Institute for Mathematics, Physics and Mechanics, Ljubljana, Slovenia

Corresponding author: Davorin Lešnik ( davorin.lesnik@fmf.uni-lj.si )

© Davorin Lešnik.
This article is freely available under the J.UCS Open Content License.
Citation: Lešnik D (2009) Constructive Urysohn Universal Metric Space. JUCS - Journal of Universal Computer Science 15(6): 1236-1263. https://doi.org/10.3217/jucs-015-06-1236
Open Access
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
constructive mathematics, metric space, Urysohn universal space