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