Kirszbraun定理和Helly定理的可定义版本

Kirszbraun定理指出：每个Lipschitz映射$S\to\mathbb R^n$（其中$S\subseteq \mathbb R^m$）都能扩张为具有相同Lipschitz常数的Lipschitz映射$\mathbb R^m \to \mathbb R^n$。其证明依赖于Helly定理：$\mathbb R^n$中每个紧子集族，若其每个至多包含$n+1$个集合的子族都有公共点，则整个族有非空交集。我们证明了这些定理在任意可定义完备的有序域扩张中对于可定义映射和集合成立的版本。