KuratowskiEmbedding.embeddingOfSubset_isometry
theorem KuratowskiEmbedding.embeddingOfSubset_isometry :
∀ {α : Type u} [inst : MetricSpace α] (x : ℕ → α),
DenseRange x → Isometry (KuratowskiEmbedding.embeddingOfSubset x)
The theorem `KuratowskiEmbedding.embeddingOfSubset_isometry` states that for any countable reference set `x` in a metric space `α`, if `x` is dense (i.e., every point in `α` is either in `x` or is a limit point of `x`), then the embedding map, which maps each point `a` in `α` to a function with codomain `ℝ` under the Kuratowski embedding, is an isometry. In other words, this embedding map preserves the distance between any two points in `x`; the edistance between any two points in the image under the embedding map is the same as their edistance in the original metric space `α`.
More concisely: For any countable, dense subset `x` in a metric space `α`, the Kuratowski embedding map preserves the distances between points in `x`.
|
KuratowskiEmbedding.exists_isometric_embedding
theorem KuratowskiEmbedding.exists_isometric_embedding :
∀ (α : Type u) [inst : MetricSpace α] [inst_1 : TopologicalSpace.SeparableSpace α], ∃ f, Isometry f
This theorem, named "KuratowskiEmbedding.exists_isometric_embedding", states that for any given separable metric space, there exists an isometric embedding into the space of bounded sequences of real numbers (`ℓ^∞(ℕ)`). An isometric embedding, or just isometry, is a transformation that preserves distance, meaning the distance between any two points in the original space is the same as the distance between their images in the target space. Therefore, the theorem ensures that any separable metric space can be faithfully represented in the space of bounded sequences without any distortion of distances.
More concisely: Every separable metric space has an isometric embedding into the space of bounded real sequences (`ℓ^∞(ℕ)`).
|
KuratowskiEmbedding.embeddingOfSubset_dist_le
theorem KuratowskiEmbedding.embeddingOfSubset_dist_le :
∀ {α : Type u} [inst : MetricSpace α] (x : ℕ → α) (a b : α),
dist (KuratowskiEmbedding.embeddingOfSubset x a) (KuratowskiEmbedding.embeddingOfSubset x b) ≤ dist a b
This theorem states that for any metric space, denoted as 'α', and any countable sequence of points in it, represented by the function 'x : ℕ → α', the Kuratowski embedding of two points 'a' and 'b' from the space 'α' always satisfies a specific property: the distance between the embeddings of these two points is less than or equal to the distance between the two original points in the metric space. In other words, the Kuratowski embedding is a semi-contraction, meaning it doesn't 'stretch' distances between points.
More concisely: For any metric space α and countable sequence of points x : ℕ → α, the Kuratowski embedding of two points a and b in α satisfies the property d(embd(a), embd(b)) ≤ d(a, b), where embd denotes the Kuratowski embedding and d the metric distance.
|
LipschitzOnWith.extend_lp_infty
theorem LipschitzOnWith.extend_lp_infty :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {ι : Type u_1} {f : α → ↥(lp (fun i => ℝ) ⊤)} {K : NNReal},
LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
The theorem `LipschitzOnWith.extend_lp_infty` states that for any function `f` mapping from a type `α` to `ℓ^∞(ι, ℝ)` (the space of bounded sequences of real numbers indexed by `ι`) which is `K`-Lipschitz continuous on a subset `s` of `α`, there exists an extension `g` of `f` to the entire space `α` that is also `K`-Lipschitz continuous. This means that `g` behaves exactly like `f` on the subset `s` (i.e., `f` and `g` are equal on `s`) and moreover, for all `x, y` in `α`, the distance between `g(x)` and `g(y)` is at most `K` times the distance between `x` and `y`. This result is referred to as Theorem 2.2 in Assaf Naor's "Metric Embeddings and Lipschitz Extensions".
More concisely: Given a `K`-Lipschitz continuous function `f` from a type `α` to `ℓ^∞(ι, ℝ)` defined on a subset `s` of `α`, there exists an extension `g` of `f` to all of `α` that is also `K`-Lipschitz continuous and agrees with `f` on `s`.
|
kuratowskiEmbedding.isometry
theorem kuratowskiEmbedding.isometry :
∀ (α : Type u) [inst : MetricSpace α] [inst_1 : TopologicalSpace.SeparableSpace α],
Isometry (kuratowskiEmbedding α)
The theorem `kuratowskiEmbedding.isometry` states that the Kuratowski embedding is an isometry for any type `α` that is a metric space and a separable space. In other words, for any two points in `α`, the distance between their images under the Kuratowski embedding in the space `ℓ^∞(ℕ, ℝ)` is the same as the original distance between the points in `α`. This theorem aligns with Theorem 2.1 from Assaf Naor's work "Metric Embeddings and Lipschitz Extensions".
More concisely: The Kuratowski embedding is an isometry between any separable metric space `α` and its image in `ℓ^∞(ℕ, ℝ)`.
|