Commit 2024-10-16 16:23 ec9e50a6

View on Github →

chore: measurable_spanningSets → measurableSet_spanningSets (#17834) This was misnamed. From GibbsMeasure

Estimated changes

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

Modified Mathlib/MeasureTheory/Decomposition/Exhaustion.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Trim.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

added theorem MeasureTheory.measurableSet_spanningSets

added theorem MeasureTheory.measurableSet_spanningSetsIndex

deleted theorem MeasureTheory.measurable_spanningSets

deleted theorem MeasureTheory.measurable_spanningSetsIndex