Commit 2024-05-06 03:42 f80fa936

View on Github →

refactor: use FunLike for OuterMeasure (#12668) Also extracts trim_anti_measurableSpace

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

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

Modified Mathlib/MeasureTheory/Measure/Haar/Quotient.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/MeasureTheory/Measure/NullMeasurable.lean

Modified Mathlib/MeasureTheory/Measure/VectorMeasure.lean

Modified Mathlib/MeasureTheory/OuterMeasure/Basic.lean

added theorem MeasureTheory.OuterMeasure.measureOf_eq_coe

added theorem MeasureTheory.OuterMeasure.trim_anti_measurableSpace

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Kernel/Condexp.lean

Modified Mathlib/Probability/Kernel/MeasureCompProd.lean

Modified Mathlib/Probability/ProbabilityMassFunction/Integrals.lean