Commit 2024-01-16 07:13 25e096f2

feat(MeasureTheory): generalize some theorem to Sort* (#9769) Generalize some theorems from {β : Type*} [Countable β] (f : β → α) to {ι : Sort*} [Countable ι] (f : ι → α). This way they automatically work for f : (p : Prop) → α.

• Generalize MeasureTheory.OuterMeasure.iUnion_null, MeasureTheory.OuterMeasure.iUnion_null_iff, MeasureTheory.measure_iUnion_null, and MeasureTheory.measure_iUnion_null_iff.
• Deprecate MeasureTheory.OuterMeasure.iUnion_null_iff' and MeasureTheory.measure_iUnion_null_iff'.
• Generalize MeasureTheory.exists_measurable_superset_forall_eq and MeasureTheory.exists_measure_pos_of_not_measure_iUnion_null.
• Reorder implicit arguments in some theorems (move ι around).