Lipschitz embeddings into ℓ^∞

[hrmacbeth]

A Lipschitz function from a subset of a space into ℓ^∞ can be extended to the whole space, with the same Lipschitz constant. See Theorem 2.2 here:
https://web.math.princeton.edu/~naor/homepage%20files/embeddings_extensions.pdf

We have this result for the ℓ^∞ space on ι for ι finite, see #11530, but it would be nice to get the result for general (potentially infinite) ι! The proof is basically the same.

Note that ℓ^∞ space is invoked in Lean as lp (λ i : ι, ℝ) ∞.