English
Every separable metric space embeds isometrically into ℓ^∞(ℕ).
Русский
Каждое разделимое метрическое пространство можно изометрически вложить в ℓ^∞(ℕ).
LaTeX
$$$\exists f:\ α \to \ell^\infty(\mathbb{N}),\ \text{Isometry} f$$$
Lean4
/-- Every separable metric space embeds isometrically in `ℓ^∞(ℕ)`. -/
theorem exists_isometric_embedding (α : Type u) [MetricSpace α] [SeparableSpace α] : ∃ f : α → ℓ^∞(ℕ), Isometry f :=
by
rcases (univ : Set α).eq_empty_or_nonempty with h | h
· use fun _ => 0; intro x; exact absurd h (Nonempty.ne_empty ⟨x, mem_univ x⟩)
· -- We construct a map x : ℕ → α with dense image
rcases h with ⟨basepoint⟩
haveI : Inhabited α := ⟨basepoint⟩
have : ∃ s : Set α, s.Countable ∧ Dense s := exists_countable_dense α
rcases this with ⟨S, ⟨S_countable, S_dense⟩⟩
rcases Set.countable_iff_exists_subset_range.1 S_countable with
⟨x, x_range⟩
-- Use embeddingOfSubset to construct the desired isometry
exact ⟨embeddingOfSubset x, embeddingOfSubset_isometry x (S_dense.mono x_range)⟩
