exists_embedding_l_infty — Mathlib

English

A T3 space with second countable topology can be embedded into the Banach space ℓ∞(ℕ, ℝ).

Русский

Т3 пространство с топологией второй счетности можно внедрить в пространство л∞(ℕ, ℝ).

LaTeX

$$$\\exists f: X \\to \\ell^{\\infty}(\\mathbb{N},\\mathbb{R}),\\; \\text{IsEmbedding}(f)$$$

Lean4

/-- A T₃ topological space with second countable topology can be embedded into `l^∞ = ℕ →ᵇ ℝ`. -/
theorem exists_embedding_l_infty : ∃ f : X → ℕ →ᵇ ℝ, IsEmbedding f :=
  let ⟨f, hf⟩ := exists_isInducing_l_infty X;
  ⟨f, hf.isEmbedding⟩

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