English
A separable metric space can be embedded into ℓ^∞(ℕ) by distances to a fixed dense countable set (Kuratowski embedding).
Русский
Разделимое метрическое пространство можно встроить в ℓ^∞(ℕ) посредством расстояний до фиксированного плотного счётного множества (встраивание Куротовского).
LaTeX
$$$\text{embeddingOfSubset}$ is a map with coordinates $\big( (\mathrm{embeddingOfSubset}(x,a))_n \big) = d(a,x_n) - d(x_0,x_n)$ and lies in $\ell^\infty(\mathbb{N})$.$$
Lean4
/-- A metric space can be embedded in `l^∞(ℝ)` via the distances to points in
a fixed countable set, if this set is dense. This map is given in `kuratowskiEmbedding`,
without density assumptions. -/
def embeddingOfSubset : ℓ^∞(ℕ) :=
⟨fun n => dist a (x n) - dist (x 0) (x n), by
apply memℓp_infty
use dist a (x 0)
rintro - ⟨n, rfl⟩
exact abs_dist_sub_le _ _ _⟩
