http://arxiv.org/abs/0906.1168

Definable versions of theorems by Kirszbraun and Helly
Matthias Aschenbrenner, Andreas Fischer
(Submitted on 5 Jun 2009 (v1), last revised 15 Jul 2010 (this version, v2))

Kirszbraun's Theorem states that every Lipschitz map S→Rn, where S⊆Rm, has an extension to a Lipschitz map Rm→Rn with the same Lipschitz constant. Its proof relies on Helly's Theorem: every family of compact subsets of Rn, having the property that each of its subfamilies consisting of at most n+1 sets share a common point, has a non-empty intersection. We prove versions of these theorems valid for definable maps and sets in arbitrary definably complete expansions of ordered fields.