# Documentation

Mathlib.Topology.MetricSpace.Kuratowski

# The Kuratowski embedding #

Any separable metric space can be embedded isometrically in ℓ^∞(ℕ, ℝ). Any partially defined Lipschitz map into ℓ^∞ can be extended to the whole space.

### Any separable metric space can be embedded isometrically in ℓ^∞(ℕ, ℝ) #

def KuratowskiEmbedding.embeddingOfSubset {α : Type u} [] (x : α) (a : α) :
{ x // x lp (fun i => ) }

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.

Instances For
theorem KuratowskiEmbedding.embeddingOfSubset_coe {α : Type u} {n : } [] (x : α) (a : α) :
= dist a (x n) - dist (x 0) (x n)
theorem KuratowskiEmbedding.embeddingOfSubset_dist_le {α : Type u} [] (x : α) (a : α) (b : α) :

The embedding map is always a semi-contraction.

theorem KuratowskiEmbedding.embeddingOfSubset_isometry {α : Type u} [] (x : α) (H : ) :

When the reference set is dense, the embedding map is an isometry on its image.

Every separable metric space embeds isometrically in ℓ^∞(ℕ).

def kuratowskiEmbedding (α : Type u) [] :
α{ x // x lp (fun i => ) }

The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℕ, ℝ).

Instances For
theorem kuratowskiEmbedding.isometry (α : Type u) [] :

The Kuratowski embedding is an isometry. Theorem 2.1 of [Assaf Naor, Metric Embeddings and Lipschitz Extensions][Naor-2015].

Version of the Kuratowski embedding for nonempty compacts

Instances For
theorem LipschitzOnWith.extend_lp_infty {α : Type u} {ι : Type u_1} {s : Set α} {f : α{ x // x lp (fun i => ) }} {K : NNReal} (hfl : ) :
g, Set.EqOn f g s

A function f : α → ℓ^∞(ι, ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space.

Theorem 2.2 of [Assaf Naor, Metric Embeddings and Lipschitz Extensions][Naor-2015]

The same result for the case of a finite type ι is implemented in LipschitzOnWith.extend_pi.