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 ℓ^∞(ℝ) #
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 : ℕ), has_dist.dist a (x n) - has_dist.dist (x 0) (x n), _⟩
theorem
Kuratowski_embedding.embedding_of_subset_coe
{α : Type u}
{n : ℕ}
[metric_space α]
(x : ℕ → α)
(a : α) :
⇑(Kuratowski_embedding.embedding_of_subset x a) n = has_dist.dist 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.
theorem
Kuratowski_embedding.embedding_of_subset_isometry
{α : Type u}
[metric_space α]
(x : ℕ → α)
(H : dense_range x) :
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 α]
[topological_space.separable_space α] :
Every separable metric space embeds isometrically in ℓ_infty_ℝ.
noncomputable
def
Kuratowski_embedding
(α : Type u)
[metric_space α]
[topological_space.separable_space α] :
The Kuratowski embedding is an isometric embedding of a separable metric space in ℓ^∞(ℝ).
Equations
@[protected]
theorem
Kuratowski_embedding.isometry
(α : Type u)
[metric_space α]
[topological_space.separable_space α] :
The Kuratowski embedding is an isometry.
def
nonempty_compacts.Kuratowski_embedding
(α : Type u)
[metric_space α]
[compact_space α]
[nonempty α] :
Version of the Kuratowski embedding for nonempty compacts
Equations
- nonempty_compacts.Kuratowski_embedding α = {to_compacts := {carrier := set.range (Kuratowski_embedding α), is_compact' := _}, nonempty' := _}