Commit 2024-10-16 13:45 8d09169a

View on Github →

chore(BorelSpace): make MeasurableSpace arguments implicit (#17819) ... rather than instance arguments. This is motivated by non-canonical sigma-algebras showing up in the theory of Gibbs measures. From GibbsMeasure

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean

modified theorem Measurable.iInf_Prop

modified theorem Measurable.iSup_Prop

modified theorem measure_eq_measure_preimage_add_measure_tsum_Ico_zpow

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean

modified theorem AEMeasurable.nnreal_tsum

modified theorem ENNReal.measurable_of_measurable_nnreal_nnreal

modified theorem ENNReal.measurable_of_measurable_nnreal_prod

modified theorem exists_spanning_measurableSet_le

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

modified theorem MeasureTheory.Measure.NullMeasurableSet.image

modified theorem MeasureTheory.Measure.QuasiMeasurePreserving.smul_ae_eq_of_ae_eq

modified theorem MeasureTheory.Measure.ae_eq_image_of_ae_eq_comap

modified theorem MeasureTheory.Measure.comap_apply

modified theorem MeasureTheory.Measure.comap_apply₀

modified theorem MeasureTheory.Measure.comap_preimage

modified theorem MeasureTheory.Measure.comapₗ_apply

modified theorem MeasureTheory.Measure.comapₗ_eq_comap

modified theorem MeasureTheory.Measure.le_comap_apply

modified theorem MeasureTheory.Measure.measure_image_eq_zero_of_comap_eq_zero

modified theorem MeasureTheory.Measure.toOuterMeasure_top

modified theorem MeasureTheory.measure_iInter_eq_iInf'

modified theorem MeasureTheory.tendsto_measure_iInter'

modified theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint

modified theorem MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀