`PhysFunctionalAnalysis.l2_separable` : TopologicalSpace.SeparableSpace (Lp ℝ 2 unitMeasure)

Proved

PhysFunctionalAnalysis.l2_separable

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.l2_separable : TopologicalSpace.SeparableSpace (Lp ℝ 2 unitMeasure)

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.l2_separable.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.l2_separable
import Mathlib
import Definitions.Def_PhysFunctionalAnalysis
import Definitions.Def_PhysMeasureBasis
import Definitions.Def_ChapterA4
open PhysMeasureBasis
open PhysFunctionalAnalysis


open MeasureTheory Set
open scoped ENNReal lp

noncomputable section


open PhysMeasureBasis

Formal statement

theorem PhysFunctionalAnalysis.l2_separable :
    TopologicalSpace.SeparableSpace (Lp ℝ 2 unitMeasure) := by sorry

View graph