`PhysFunctionalAnalysis.hilbert_classification` (E F : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] [NormedAddCommGro

Proved

PhysFunctionalAnalysis.hilbert_classification

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.hilbert_classification (E F : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F] [TopologicalSpace.SeparableSpace F] (hE : ¬ FiniteDimensional ℝ E) (hF : ¬ FiniteDimensional ℝ F) : Nonempty (E ≃ₗᵢ[ℝ] F)

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.hilbert_classification.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.hilbert_classification
import Mathlib
import Definitions.Def_PhysFunctionalAnalysis
import Definitions.Def_ChapterA4
open PhysFunctionalAnalysis


open MeasureTheory Set
open scoped ENNReal lp

noncomputable section


open PhysMeasureBasis

Formal statement

theorem PhysFunctionalAnalysis.hilbert_classification (E F : Type*)
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [TopologicalSpace.SeparableSpace E]
    [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
    [TopologicalSpace.SeparableSpace F]
    (hE : ¬ FiniteDimensional ℝ E) (hF : ¬ FiniteDimensional ℝ F) :
    Nonempty (E ≃ₗᵢ[ℝ] F) := by sorry

View graph