Commit 2025-06-23 17:18 c9a15699

refactor(MeasureTheory/PMF): Removing MasurableSet hypotheses (#26230) This commit introduces the following generalizations:

• toMeasure_mono no longer requires the target set t to be measurable.
• toMeasure_apply_inter_support no longer requires p.support to be measurable.
• restrict_toMeasure_support no longer requires a [MeasurableSingletonClass α] instance. In the [MeasurableSingletonClass α] context, a new lemma toMeasure_apply_eq_toOuterMeasure is added. It shows that p.toMeasure s = p.toOuterMeasure s for any set s. This lemma is then used to shorten the proofs for:
• toMeasure_apply_finset
• toMeasure_apply_fintype A new lemma toMeasure_apply_eq_tsum replaces toMeasure_apply_of_finite, since the finite assumption is no longer required. Additionally, as suggested during review, the argument s : Set α is now implicit in several lemmas, as it is inferable from the hs : MeasurableSet s hypothesis.