Commit 2023-11-11 01:53 76efc30c

View on Github →

feat: measurability of uniqueElim and piFinsetUnion (#8249)

The extra import doesn't add any additional imports transitively
Also use implicit arguments for some MeasurableSpace arguments for consistency with other lemmas.
Redefine Equiv.piSubsingleton and MulEquiv.piSubsingleton to Equiv.piUnique and MulEquiv.piUnique.

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

deleted def MulEquiv.piSubsingleton

added def MulEquiv.piUnique

Modified Mathlib/GroupTheory/Sylow.lean

deleted theorem Sylow.subsingleton_of_normal

Modified Mathlib/Logic/Equiv/Defs.lean

modified def Equiv.funUnique

deleted def Equiv.piSubsingleton

added def Equiv.piUnique

Modified Mathlib/Logic/Unique.lean

added theorem uniqueElim_const

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

modified theorem MeasureTheory.measurePreserving_funUnique

added theorem MeasureTheory.measurePreserving_piFinsetUnion

added theorem MeasureTheory.measurePreserving_piUnique

modified theorem MeasureTheory.measurePreserving_sumPiEquivProdPi

modified theorem MeasureTheory.measurePreserving_sumPiEquivProdPi_symm

added theorem MeasureTheory.volume_preserving_piFinsetUnion

added theorem MeasureTheory.volume_preserving_piUnique

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

modified def MeasurableEquiv.funUnique

added def MeasurableEquiv.piFinsetUnion

added def MeasurableEquiv.piUnique

added theorem measurable_uniqueElim

added theorem measurable_updateFinset