Commit 2024-05-09 10:48 51625e90

View on Github →

refactor(Measure): use FunLike (#12684)

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

Modified Mathlib/MeasureTheory/Decomposition/Jordan.lean

Modified Mathlib/MeasureTheory/Decomposition/Lebesgue.lean

Modified Mathlib/MeasureTheory/Group/FundamentalDomain.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/EverywherePos.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

modified theorem MeasureTheory.FiniteMeasure.coeFn_zero

Modified Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean

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

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

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

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

added theorem MeasureTheory.Measure.coe_toOuterMeasure

added theorem MeasureTheory.Measure.toOuterMeasure_apply

modified theorem MeasureTheory.Measure.toOuterMeasure_injective

modified theorem MeasureTheory.measure_eq_trim

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

Modified Mathlib/MeasureTheory/Measure/Restrict.lean

modified theorem MeasureTheory.Measure.restrict_apply₀

Modified Mathlib/MeasureTheory/Measure/Tilted.lean

Modified Mathlib/MeasureTheory/Measure/Trim.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Kernel/Composition.lean

Modified Mathlib/Probability/Kernel/Disintegration/Density.lean

Modified Mathlib/Probability/Kernel/RadonNikodym.lean

Modified Mathlib/Probability/Variance.lean