Commit 2024-05-18 07:32 78232185

View on Github →

feat(MeasureTheory): generalize some lemmas to OuterMeasureClass (#13002)

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Integrability.lean

Modified Mathlib/MeasureTheory/Covering/Differentiation.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

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

Modified Mathlib/MeasureTheory/Integral/Layercake.lean

Modified Mathlib/MeasureTheory/Measure/Content.lean

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

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

deleted theorem MeasureTheory.measure_diff_null

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

deleted theorem MeasureTheory.measure_biUnion_finset_le

deleted theorem MeasureTheory.measure_biUnion_le

deleted theorem MeasureTheory.measure_biUnion_null_iff

deleted theorem MeasureTheory.measure_empty

deleted theorem MeasureTheory.measure_iUnion_fintype_le

deleted theorem MeasureTheory.measure_iUnion_le

deleted theorem MeasureTheory.measure_iUnion_null

deleted theorem MeasureTheory.measure_iUnion_null_iff

deleted theorem MeasureTheory.measure_mono

deleted theorem MeasureTheory.measure_mono_null

deleted theorem MeasureTheory.measure_sUnion_null_iff

deleted theorem MeasureTheory.measure_union_le

deleted theorem MeasureTheory.measure_union_null

deleted theorem MeasureTheory.measure_union_null_iff

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

deleted theorem MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure

deleted theorem MeasureTheory.null_of_locally_null

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

modified theorem MeasureTheory.OuterMeasure.diff_null

modified theorem MeasureTheory.OuterMeasure.empty'

modified theorem MeasureTheory.OuterMeasure.mono'

added theorem MeasureTheory.exists_mem_forall_mem_nhdsWithin_pos_measure

added theorem MeasureTheory.measure_biUnion_finset_le

added theorem MeasureTheory.measure_biUnion_le

added theorem MeasureTheory.measure_biUnion_null_iff

added theorem MeasureTheory.measure_diff_null

added theorem MeasureTheory.measure_empty

added theorem MeasureTheory.measure_iUnion_fintype_le

added theorem MeasureTheory.measure_iUnion_le

added theorem MeasureTheory.measure_iUnion_null_iff

added theorem MeasureTheory.measure_iUnion_of_tendsto_zero

added theorem MeasureTheory.measure_le_inter_add_diff

added theorem MeasureTheory.measure_mono

added theorem MeasureTheory.measure_mono_null

added theorem MeasureTheory.measure_null_of_locally_null

added theorem MeasureTheory.measure_pos_of_superset

added theorem MeasureTheory.measure_sUnion_null_iff

added theorem MeasureTheory.measure_union_le

added theorem MeasureTheory.measure_union_null

added theorem MeasureTheory.measure_union_null_iff

Modified Mathlib/MeasureTheory/OuterMeasure/Caratheodory.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Induced.lean

Modified Mathlib/MeasureTheory/OuterMeasure/OfFunction.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Operations.lean