Discontinuous linear functionals

TheoremA discontinuous linear functional on an infinite-dimensional normed space#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). If \(E\) is not finite-dimensional, then there exists a linear functional \(f \colon E \to \mathbb{K}\) that is not continuous.

theorem exists_discontinuous_linearMap_of_not_finiteDimensional
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    (hE : ¬ FiniteDimensional 𝕜 E) :
    ∃ f : E →ₗ[𝕜] 𝕜, ¬ Continuous f

Used by 2

Used byThe algebraic dual is strictly larger than the topological dual · Every linear functional is continuous if and only if the space is finite-dimensional

TheoremEvery linear functional is continuous if and only if the space is finite-dimensional#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). Every linear functional \(f \colon E \to \mathbb{K}\) is continuous if and only if \(E\) is finite-dimensional.

theorem forall_linearMap_continuous_iff_finiteDimensional
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] :
    (∀ f : E →ₗ[𝕜] 𝕜, Continuous f) ↔ FiniteDimensional 𝕜 E

Uses 1

Proof usesA discontinuous linear functional on an infinite-dimensional normed space

TheoremThe algebraic dual is strictly larger than the topological dual#✓fully proved

Let \(E\) be a normed space over \(\mathbb{K} = \mathbb{R}\) or \(\mathbb{C}\). If \(E\) is not finite-dimensional, then there is a linear functional \(f \colon E \to \mathbb{K}\) that differs from every continuous linear functional \(g \colon E \to \mathbb{K}\).

theorem exists_linearMap_not_continuousLinearMap
    {𝕜 : Type*} [RCLike 𝕜]
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    (hE : ¬ FiniteDimensional 𝕜 E) :
    ∃ f : E →ₗ[𝕜] 𝕜, ∀ g : E →L[𝕜] 𝕜, f ≠ (g : E →ₗ[𝕜] 𝕜)

Uses 1

Proof usesA discontinuous linear functional on an infinite-dimensional normed space

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.