`PhysFunctionalAnalysis.exists_l2_iso` (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] (hE : ¬ FiniteDimensional ℝ

Proved

PhysFunctionalAnalysis.exists_l2_iso

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.exists_l2_iso (E : Type*) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [TopologicalSpace.SeparableSpace E] (hE : ¬ FiniteDimensional ℝ E) : Nonempty (E ≃ₗᵢ[ℝ] ℓ²(ℕ, ℝ))

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.exists_l2_iso.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.exists_l2_iso
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.exists_l2_iso (E : Type*)
    [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
    [TopologicalSpace.SeparableSpace E] (hE : ¬ FiniteDimensional ℝ E) :
    Nonempty (E ≃ₗᵢ[ℝ] ℓ²(ℕ, ℝ)) := by sorry

View graph