`PhysMeasureBasis.null_singleton` {α : Type*} [MeasurableSpace α] (μ : Measure α) [MeasurableSingletonClass α] [NullSingletonClass μ] (a : α) : μ {a} = 0

Proved

PhysMeasureBasis.null_singleton

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysMeasureBasis.

PhysMeasureBasis.null_singleton {α : Type*} [MeasurableSpace α] (μ : Measure α) [MeasurableSingletonClass α] [NullSingletonClass μ] (a : α) : μ {a} = 0

Formalization note: Lean 4 identifier PhysMeasureBasis.null_singleton.

Preamble

-- Generated from PhysMeasureBasis.lean — theorem PhysMeasureBasis.null_singleton
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.null_singleton {α : Type*} [MeasurableSpace α] (μ : Measure α)
    [MeasurableSingletonClass α] [NullSingletonClass μ] (a : α) : μ {a} = 0 := by sorry

View graph