Compact operators and finite dimensional spaces #
This file contains results linking IsCompactOperator with FiniteDimensional.
The motivation for not including this in the same file as the definition of compact operators
is that Mathlib.Topology.Algebra.Module.FiniteDimension is quite a heavy import to add there.
theorem
isCompactOperator_id_iff_finiteDimensional
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[T2Space E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
[LocallyCompactSpace 𝕜]
:
theorem
FiniteDimensional.of_isCompactOperator_id
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[T2Space E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(h : IsCompactOperator id)
:
If the identity operator of a Banach space over a nontrivially normed field is compact, then the space is finite dimensional.
@[deprecated FiniteDimensional.of_isCompactOperator_id (since := "2026-03-05")]
theorem
IsCompactOperator.finiteDimensional
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
[CompleteSpace 𝕜]
{E : Type u_2}
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[T2Space E]
[IsTopologicalAddGroup E]
[ContinuousSMul 𝕜 E]
(h : IsCompactOperator id)
:
Alias of FiniteDimensional.of_isCompactOperator_id.
If the identity operator of a Banach space over a nontrivially normed field is compact, then the space is finite dimensional.