Commit 2024-06-01 12:34 8a34ed01

View on Github →

refactor: Use FunLike on ProbabilityMeasure (#13171) ... instead of CoeFun. This ensures ⇑μ doesn't get unfolded to fun s ↦ (μ s).toNNReal, which is bad for both readability in the infoview and indexing in simp (see #13164 for the latter).

Estimated changes

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

added theorem MeasureTheory.FiniteMeasure.coeFn_def

added theorem MeasureTheory.FiniteMeasure.coeFn_mk

deleted theorem MeasureTheory.FiniteMeasure.coeFn_smul_apply

modified theorem MeasureTheory.FiniteMeasure.coeFn_zero

added theorem MeasureTheory.FiniteMeasure.mk_apply

added theorem MeasureTheory.FiniteMeasure.smul_apply

Modified Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean

modified theorem MeasureTheory.FiniteMeasure.map_fst_prod

modified theorem MeasureTheory.FiniteMeasure.map_snd_prod

modified theorem MeasureTheory.FiniteMeasure.prod_prod

modified theorem MeasureTheory.ProbabilityMeasure.prod_prod

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean

added theorem MeasureTheory.ProbabilityMeasure.coeFn_def

added theorem MeasureTheory.ProbabilityMeasure.coeFn_mk

added theorem MeasureTheory.ProbabilityMeasure.coeFn_toFiniteMeasure

added theorem MeasureTheory.ProbabilityMeasure.mk_apply

added theorem MeasureTheory.ProbabilityMeasure.toFiniteMeasure_apply