`PhysMeasureBasis.atomless_mutuallySingular_atomic` {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [NullSingletonClass μ] {A : Set α} (hA : A.Counta

Proved

PhysMeasureBasis.atomless_mutuallySingular_atomic

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysMeasureBasis.

PhysMeasureBasis.atomless_mutuallySingular_atomic {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ ν : Measure α) [NullSingletonClass μ] {A : Set α} (hA : A.Countable) (hν : ν Aᶜ = 0) : μ ⟂ₘ ν

Formalization note: Lean 4 identifier PhysMeasureBasis.atomless_mutuallySingular_atomic.

Preamble

-- Generated from PhysMeasureBasis.lean — theorem PhysMeasureBasis.atomless_mutuallySingular_atomic
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.atomless_mutuallySingular_atomic {α : Type*} [MeasurableSpace α]
    [MeasurableSingletonClass α] (μ ν : Measure α) [NullSingletonClass μ]
    {A : Set α} (hA : A.Countable) (hν : ν Aᶜ = 0) :
    μ ⟂ₘ ν := by sorry

View graph