  We develop a version of Herbrand's theorem for continuous logic and use it to
prove that definable functions in infinite-dimensional Hilbert spaces are
piecewise approximable by affine functions. We obtain similar results for
definable functions in Hilbert spaces expanded by a group of generic unitary
operators and Hilbert spaces expanded by a generic subspace. We also show how
Herbrand's theorem can be used to characterize definable functions in some
absolutely ubiquitous structures from classical logic.
