The Kuratowski embedding #

Any separable metric space can be embedded isometrically in ℓ^∞(ℝ).

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

def Kuratowski_embedding.embedding_of_subset {α : Type u} [metric_space α] (x : ℕ → α) (a : α) :

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 Kuratowski_embedding, without density assumptions.

Equations

Kuratowski_embedding.embedding_of_subset x a = ⟨λ (n : ℕ), dist a (x n) - dist (x 0) (x n), _⟩

source

theorem Kuratowski_embedding.embedding_of_subset_coe {α : Type u} {n : ℕ} [metric_space α] (x : ℕ → α) (a : α) :

⇑(Kuratowski_embedding.embedding_of_subset x a) n = dist a (x n) - dist (x 0) (x n)

source

theorem Kuratowski_embedding.embedding_of_subset_dist_le {α : Type u} [metric_space α] (x : ℕ → α) (a b : α) :

dist (Kuratowski_embedding.embedding_of_subset x a) (Kuratowski_embedding.embedding_of_subset x b) ≤ dist a b

The embedding map is always a semi-contraction.

source

theorem Kuratowski_embedding.embedding_of_subset_isometry {α : Type u} [metric_space α] (x : ℕ → α) (H : dense_range x) :

isometry (Kuratowski_embedding.embedding_of_subset x)

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

source

theorem Kuratowski_embedding.exists_isometric_embedding (α : Type u) [metric_space α] [topological_space.separable_space α] :

∃ (f : α → ↥(lp (λ (n : ℕ), ℝ) ⊤)), isometry f

Every separable metric space embeds isometrically in ℓ_infty_ℝ.

source

noncomputable def Kuratowski_embedding (α : Type u) [metric_space α] [topological_space.separable_space α] :

α → ↥(lp (λ (n : ℕ), ℝ) ⊤)

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

Equations

Kuratowski_embedding α = classical.some _

source

@[protected]

theorem Kuratowski_embedding.isometry (α : Type u) [metric_space α] [topological_space.separable_space α] :

isometry (Kuratowski_embedding α)

The Kuratowski embedding is an isometry.

source

def nonempty_compacts.Kuratowski_embedding (α : Type u) [metric_space α] [compact_space α] [nonempty α] :

topological_space.nonempty_compacts ↥(lp (λ (n : ℕ), ℝ) ⊤)

Version of the Kuratowski embedding for nonempty compacts

Equations

nonempty_compacts.Kuratowski_embedding α = ⟨set.range (Kuratowski_embedding α), _⟩