Commit 2025-11-26 15:01 c081da6a

View on Github →

feat(MeasureTheory): typeclass for measurability of equality (#31512) Currently, there are multiple lemmas of the form MeasurableSet {x | f x = g x} with different typeclass assumptions. This PR unifies them using a new MeasurableEq typeclass. A new instance for second-countable Hausdorff spaces is also added.

Estimated changes

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

Modified Mathlib/MeasureTheory/Group/Arithmetic.lean

deleted theorem ae_eq_trim_of_measurable

deleted theorem measurableSet_eq_fun'

deleted theorem measurableSet_eq_fun

deleted theorem measurableSet_eq_fun_of_countable

deleted theorem nullMeasurableSet_eq_fun

Modified Mathlib/MeasureTheory/MeasurableSpace/Constructions.lean

added theorem Measurable.const_eq

added theorem Measurable.eq

added theorem Measurable.eq_const

added theorem measurableSet_eq_fun

Modified Mathlib/MeasureTheory/MeasurableSpace/Defs.lean

Modified Mathlib/MeasureTheory/Measure/AEMeasurable.lean

added theorem nullMeasurableSet_eq_fun

Modified Mathlib/MeasureTheory/Measure/Trim.lean

added theorem ae_eq_trim_of_measurable

Modified Mathlib/Probability/Kernel/CondDistrib.lean

modified theorem ProbabilityTheory.condExp_ae_eq_integral_condDistrib'

Modified Mathlib/Probability/Kernel/Posterior.lean