`PhysMeasureBasis.cond_diffuse_noAtoms` {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] (_hpos : μ {x | μ {x} ≠ 0}ᶜ ≠ 0) : NullSing

Proved

PhysMeasureBasis.cond_diffuse_noAtoms

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysMeasureBasis.

PhysMeasureBasis.cond_diffuse_noAtoms {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] (_hpos : μ {x | μ {x} ≠ 0}ᶜ ≠ 0) : NullSingletonClass ((μ {x | μ {x} ≠ 0}ᶜ)⁻¹ • μ.restrict {x | μ {x} ≠ 0}ᶜ)

Formalization note: Lean 4 identifier PhysMeasureBasis.cond_diffuse_noAtoms.

Preamble

-- Generated from PhysMeasureBasis.lean — theorem PhysMeasureBasis.cond_diffuse_noAtoms
import Mathlib
import Definitions.Def_PhysMeasureBasis
import Definitions.Def_ChapterA4
open PhysMeasureBasis


open MeasureTheory Set ProbabilityTheory
open scoped ENNReal

noncomputable section

Formal statement

theorem PhysMeasureBasis.cond_diffuse_noAtoms {α : Type*} [MeasurableSpace α]
    [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ]
    (_hpos : μ {x | μ {x} ≠ 0}ᶜ ≠ 0) :
    NullSingletonClass ((μ {x | μ {x} ≠ 0}ᶜ)⁻¹ • μ.restrict {x | μ {x} ≠ 0}ᶜ) := by sorry

View graph