`PhysFunctionalAnalysis.linf_not_separable` : ¬ TopologicalSpace.SeparableSpace (Lp ℝ ⊤ unitMeasure)

Proved

PhysFunctionalAnalysis.linf_not_separable

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysFunctionalAnalysis.

PhysFunctionalAnalysis.linf_not_separable : ¬ TopologicalSpace.SeparableSpace (Lp ℝ ⊤ unitMeasure)

Formalization note: Lean 4 identifier PhysFunctionalAnalysis.linf_not_separable.

Preamble

-- Generated from PhysFunctionalAnalysis.lean — theorem PhysFunctionalAnalysis.linf_not_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.linf_not_separable :
    ¬ TopologicalSpace.SeparableSpace (Lp ℝ ⊤ unitMeasure) := by sorry

View graph