Commit 2026-06-22 10:16 3ee3f85e

View on Github →

refactor(MeasureTheory/Measure/Typeclasses/NoAtoms): rename NoAtoms to NullSingletonClass (#40809) Rename the class NoAtoms to NullSingletonClass as discussed here and change all derivative names.

Estimated changes

Modified Counterexamples/Phillips.lean

Modified Mathlib.lean

Modified Mathlib/Analysis/Convolution.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

modified theorem tendsto_measure_Icc

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

modified theorem MeasureTheory.Measure.ae_eval_ne

modified theorem MeasureTheory.Measure.pi_hyperplane

deleted theorem MeasureTheory.Measure.pi_noAtoms

added theorem MeasureTheory.Measure.pi_nullSingletonClass

Modified Mathlib/MeasureTheory/Constructions/UnitInterval.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

modified theorem MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ici

modified theorem MeasureTheory.IntegrableOn.continuousOn_Ici_primitive_Ioi

modified theorem MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iic

modified theorem MeasureTheory.IntegrableOn.continuousOn_Iic_primitive_Iio

Modified Mathlib/MeasureTheory/Integral/IntegrableOn.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/IntervalAverage.lean

deleted theorem exists_eq_interval_average_of_noAtoms

added theorem exists_eq_interval_average_of_nullSingletonClass

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

modified theorem IntervalIntegrable.congr_codiscreteWithin

modified theorem IntervalIntegrable.congr_uIoo

modified theorem intervalIntegrable_congr_codiscreteWithin

modified theorem intervalIntegrable_congr_uIoo

modified theorem intervalIntegrable_iff'

modified theorem intervalIntegrable_iff_integrableOn_Icc_of_le

modified theorem intervalIntegrable_iff_integrableOn_Ico_of_le

modified theorem intervalIntegrable_iff_integrableOn_Ioo_of_le

modified theorem intervalIntegral.integral_Ici_sub_Ici'

modified theorem intervalIntegral.integral_Iio_sub_Iio'

modified theorem intervalIntegral.integral_congr_Ioo_of_le

modified theorem intervalIntegral.integral_congr_uIoo

modified theorem intervalIntegral.integral_mono_on_of_le_Ioo

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

modified theorem MeasureTheory.mutuallySingular_dirac

Modified Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

deleted theorem MeasureTheory.Measure.noAtoms_hausdorff

added theorem MeasureTheory.Measure.nullSingletonClass_hausdorff

Modified Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean

modified theorem ae_of_mem_of_ae_of_mem_inter_Ioo

modified theorem ae_restrict_of_ae_restrict_inter_Ioo

Modified Mathlib/MeasureTheory/Measure/OpenPos.lean

Modified Mathlib/MeasureTheory/Measure/Prod.lean

Renamed Mathlib/MeasureTheory/Measure/Typeclasses/NoAtoms.lean to Mathlib/MeasureTheory/Measure/Typeclasses/NullSingletonClass.lean

modified theorem Finset.measure_zero

modified theorem MeasureTheory.Measure.ae_ne

deleted theorem MeasureTheory.exists_accPt_of_noAtoms

added theorem MeasureTheory.exists_accPt_of_nullSingletonClass

modified theorem Set.Countable.ae_notMem

modified theorem Set.Countable.measure_restrict_compl

modified theorem Set.Countable.measure_zero

modified theorem Set.Finite.measure_zero

modified theorem Set.Subsingleton.measure_zero

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/MeasureTheory/Topology.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/Probability/Distributions/Gaussian/Fernique.lean

deleted theorem ProbabilityTheory.IsGaussian.noAtoms

added theorem ProbabilityTheory.IsGaussian.nullSingletonClass

Modified Mathlib/Probability/Distributions/Gaussian/Real.lean

deleted theorem ProbabilityTheory.noAtoms_gaussianReal

added theorem ProbabilityTheory.nullSingletonClass_gaussianReal

Modified scripts/nolints_prime_decls.txt