Commit 2025-03-05 21:20 fcbc2603

chore(MeasureTheory): rename pi family from π to X (#22604) Only in files that mentioned such a family, via a script:

git grep -e "π : . → Type" --name-only | rg "Measure" | xargs -I{} sed -i -e 's/π/X/g' {}

Estimated changes

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

modified theorem pi_le_borel_pi

Modified Mathlib/MeasureTheory/Constructions/Cylinders.lean

modified theorem MeasureTheory.Measurable.eval_cylinderEvents

modified def MeasureTheory.cylinderEvents

modified theorem MeasureTheory.cylinderEvents_le_pi

modified theorem MeasureTheory.cylinderEvents_mono

modified theorem MeasureTheory.cylinderEvents_univ

modified theorem MeasureTheory.measurable_cylinderEvents_iff

modified theorem MeasureTheory.measurable_cylinderEvents_lambda

modified theorem MeasureTheory.measurable_update_cylinderEvents

modified theorem MeasureTheory.measurable_update_cylinderEvents_left

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

modified theorem MeasureTheory.Measure.tprod_cons

modified theorem MeasureTheory.Measure.tprod_nil

modified theorem MeasureTheory.Measure.tprod_tprod

modified theorem MeasureTheory.measurePreserving_piUnique

modified theorem MeasureTheory.measurePreserving_sumPiEquivProdPi

modified theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm

modified theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi

modified theorem MeasureTheory.volume_measurePreserving_sumPiEquivProdPi_symm

modified theorem MeasureTheory.volume_preserving_piUnique

Modified Mathlib/MeasureTheory/Integral/Marginal.lean

modified theorem MeasureTheory.lintegral_eq_lmarginal_univ

modified theorem MeasureTheory.lintegral_eq_of_lmarginal_eq

modified theorem MeasureTheory.lintegral_le_of_lmarginal_le

modified def MeasureTheory.lmarginal

modified theorem MeasureTheory.lmarginal_congr

modified theorem MeasureTheory.lmarginal_empty

modified theorem MeasureTheory.lmarginal_eq_of_subset

modified theorem MeasureTheory.lmarginal_erase'

modified theorem MeasureTheory.lmarginal_erase

modified theorem MeasureTheory.lmarginal_insert'

modified theorem MeasureTheory.lmarginal_insert

modified theorem MeasureTheory.lmarginal_le_of_subset

modified theorem MeasureTheory.lmarginal_mono

modified theorem MeasureTheory.lmarginal_singleton

modified theorem MeasureTheory.lmarginal_union'

modified theorem MeasureTheory.lmarginal_union

modified theorem MeasureTheory.lmarginal_univ

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

modified theorem Finset.measurable_restrict

modified theorem Measurable.eq_mp

modified theorem Measurable.eval

modified theorem MeasurableSet.tProd

modified theorem Set.measurable_restrict

modified theorem measurableSet_pi

modified theorem measurableSet_pi_of_nonempty

modified theorem measurable_eq_mp

modified theorem measurable_piCongrLeft

modified theorem measurable_pi_apply

modified theorem measurable_pi_iff

modified theorem measurable_pi_lambda

modified theorem measurable_tProd_mk

modified theorem measurable_update

modified theorem measurable_updateFinset

modified theorem measurable_updateFinset_left

modified theorem measurable_update_left

Modified Mathlib/Probability/Process/Filtration.lean

modified def MeasureTheory.Filtration.cylinderEventsCompl