mathlib3documentation

topology.metric_space.kuratowski

The Kuratowski embedding #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 : α) :
(lp (λ (n : ), ) )

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
theorem Kuratowski_embedding.embedding_of_subset_coe {α : Type u} {n : } [metric_space α] (x : α) (a : α) :
= (x n) - has_dist.dist (x 0) (x n)
theorem Kuratowski_embedding.embedding_of_subset_dist_le {α : Type u} [metric_space α] (x : α) (a b : α) :

The embedding map is always a semi-contraction.

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

theorem Kuratowski_embedding.exists_isometric_embedding (α : Type u) [metric_space α]  :
(f : α (lp (λ (n : ), ) )),

Every separable metric space embeds isometrically in ℓ_infty_ℝ.

noncomputable def Kuratowski_embedding (α : Type u) [metric_space α]  :
α (lp (λ (n : ), ) )

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

Equations
@[protected]
theorem Kuratowski_embedding.isometry (α : Type u) [metric_space α]  :

The Kuratowski embedding is an isometry.

Version of the Kuratowski embedding for nonempty compacts

Equations