exists_hilbertBasis — Mathlib

English

As above: there exist w and b with s ⊆ w and b representing inclusion.

Русский

Как и выше: существуют w и b, такие что s ⊆ w и b представляет включение.

LaTeX

$$$\\exists w\\,\\exists b : HilbertBasis\\,w\\, 𝕜 E,\\ s \\subseteq w \\land \\; (b) = \\iota_w$$$

Lean4

/-- A Hilbert space admits a Hilbert basis. -/
theorem _root_.exists_hilbertBasis : ∃ (w : Set E) (b : HilbertBasis w 𝕜 E), ⇑b = ((↑) : w → E) :=
  let ⟨w, hw, _, hw''⟩ := (orthonormal_empty 𝕜 E).exists_hilbertBasis_extension
  ⟨w, hw, hw''⟩

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