`PhysMeasureBasis.countable_atoms` {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] : {x | μ {x} ≠ 0}.Countable

Proved

PhysMeasureBasis.countable_atoms

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

theoremstimepiece

Prove the following Lean 4 theorem from PhysMeasureBasis.

PhysMeasureBasis.countable_atoms {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (μ : Measure α) [IsFiniteMeasure μ] : {x | μ {x} ≠ 0}.Countable

Formalization note: Lean 4 identifier PhysMeasureBasis.countable_atoms.

Preamble

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

View graph