kuratowskiEmbedding — Mathlib

English

There exists an isometric embedding of a separable metric space into ℓ^∞(ℕ).

Русский

Существует изометрическое вложение разделимого метрического пространства в ℓ^∞(ℕ).

LaTeX

$$$\exists f:\ α \to \ell^\infty(\mathbb{N}), \text{Isometry } f$$$

Lean4

/-- The Kuratowski embedding is an isometric embedding of a separable metric space in `ℓ^∞(ℕ, ℝ)`.
-/
def kuratowskiEmbedding (α : Type u) [MetricSpace α] [SeparableSpace α] : α → ℓ^∞(ℕ) :=
  Classical.choose (KuratowskiEmbedding.exists_isometric_embedding α)

Похожие утверждения