Hamel bases of Banach spaces

TheoremA Banach space with a countable Hamel basis is finite-dimensional#✓fully proved

If E is a complete normed space over 𝕜 = ℝ, ℂ admitting a Hamel basis indexed by a countable type, then E is finite-dimensional. Completeness is essential: it is what the Baire category argument uses.

theorem finiteDimensional_of_countable_basis {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    {ι : Type*} [Countable ι] (b : Module.Basis ι 𝕜 E) : FiniteDimensional 𝕜 E

Used by 1

Used byAn infinite-dimensional Banach space has no countable Hamel basis

TheoremAn infinite-dimensional Banach space has no countable Hamel basis#✓fully proved

Let \(E\) be a complete normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). If \(E\) is not finite-dimensional, then no Hamel basis of \(E\) is indexed by a countable set.

theorem not_countable_basis_of_not_finiteDimensional {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E]
    (hE : ¬ FiniteDimensional 𝕜 E) {ι : Type*} (b : Module.Basis ι 𝕜 E) :
    ¬ Countable ι

Uses 1

Proof usesA Banach space with a countable Hamel basis is finite-dimensional

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.