Commit 2024-06-19 09:36 572940c6

View on Github →

chore: Split large file MeasureTheory.MeasurableSpace.Basic (#13937)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/MeasureTheory/MeasurableSpace/Basic.lean

deleted theorem MeasurableEmbedding.comap_eq

deleted theorem MeasurableEmbedding.comp

deleted theorem MeasurableEmbedding.exists_measurable_extend

deleted theorem MeasurableEmbedding.id

deleted theorem MeasurableEmbedding.iff_comap_eq

deleted theorem MeasurableEmbedding.measurableSet_image

deleted theorem MeasurableEmbedding.measurableSet_preimage

deleted theorem MeasurableEmbedding.measurableSet_range

deleted theorem MeasurableEmbedding.measurable_comp_iff

deleted theorem MeasurableEmbedding.measurable_extend

deleted theorem MeasurableEmbedding.measurable_rangeSplitting

deleted theorem MeasurableEmbedding.of_measurable_inverse

deleted theorem MeasurableEmbedding.of_measurable_inverse_on_range

deleted theorem MeasurableEmbedding.subtype_coe

deleted structure MeasurableEmbedding

deleted def MeasurableEquiv.Set.prod

deleted def MeasurableEquiv.Set.rangeInl

deleted def MeasurableEquiv.Set.rangeInr

deleted def MeasurableEquiv.Set.singleton

deleted def MeasurableEquiv.Set.univ

deleted def MeasurableEquiv.Simps.apply

deleted def MeasurableEquiv.Simps.symm_apply

deleted theorem MeasurableEquiv.apply_symm_apply

deleted theorem MeasurableEquiv.coe_mk

deleted theorem MeasurableEquiv.coe_piCongrLeft

deleted theorem MeasurableEquiv.coe_sumPiEquivProdPi

deleted theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm

deleted theorem MeasurableEquiv.coe_toEquiv

deleted theorem MeasurableEquiv.coe_toEquiv_symm

deleted theorem MeasurableEquiv.coe_trans

deleted theorem MeasurableEquiv.eq_image_iff_symm_image_eq

deleted theorem MeasurableEquiv.ext

deleted def MeasurableEquiv.finTwoArrow

deleted def MeasurableEquiv.funUnique

deleted theorem MeasurableEquiv.image_eq_preimage

deleted theorem MeasurableEquiv.image_preimage

deleted theorem MeasurableEquiv.image_symm

deleted theorem MeasurableEquiv.map_eq

deleted theorem MeasurableEquiv.measurableSet_image

deleted theorem MeasurableEquiv.measurableSet_preimage

deleted def MeasurableEquiv.ofInvolutive

deleted theorem MeasurableEquiv.ofInvolutive_apply

deleted theorem MeasurableEquiv.ofInvolutive_symm

deleted def MeasurableEquiv.ofUniqueOfUnique

deleted def MeasurableEquiv.piCongrLeft

deleted theorem MeasurableEquiv.piCongrLeft_apply_apply

deleted def MeasurableEquiv.piCongrRight

deleted def MeasurableEquiv.piEquivPiSubtypeProd

deleted def MeasurableEquiv.piFinSuccAbove

deleted def MeasurableEquiv.piFinTwo

deleted def MeasurableEquiv.piFinsetUnion

deleted def MeasurableEquiv.piMeasurableEquivTProd

deleted def MeasurableEquiv.piOptionEquivProd

deleted def MeasurableEquiv.piUnique

deleted theorem MeasurableEquiv.preimage_image

deleted theorem MeasurableEquiv.preimage_symm

deleted def MeasurableEquiv.prodAssoc

deleted def MeasurableEquiv.prodComm

deleted def MeasurableEquiv.prodCongr

deleted def MeasurableEquiv.prodSumDistrib

deleted def MeasurableEquiv.refl

deleted theorem MeasurableEquiv.self_comp_symm

deleted theorem MeasurableEquiv.self_trans_symm

deleted def MeasurableEquiv.sumCompl

deleted def MeasurableEquiv.sumCongr

deleted def MeasurableEquiv.sumPiEquivProdPi

deleted def MeasurableEquiv.sumProdDistrib

deleted def MeasurableEquiv.sumProdSum

deleted def MeasurableEquiv.symm

deleted theorem MeasurableEquiv.symm_apply_apply

deleted theorem MeasurableEquiv.symm_bijective

deleted theorem MeasurableEquiv.symm_comp_self

deleted theorem MeasurableEquiv.symm_mk

deleted theorem MeasurableEquiv.symm_preimage_preimage

deleted theorem MeasurableEquiv.symm_refl

deleted theorem MeasurableEquiv.symm_symm

deleted theorem MeasurableEquiv.symm_trans_self

deleted theorem MeasurableEquiv.toEquiv_injective

deleted def MeasurableEquiv.trans

deleted def MeasurableEquiv.ulift.{u,

deleted structure MeasurableEquiv

deleted theorem MeasurableSet.exists_measurable_proj

deleted theorem MeasurableSpace.comap_compl

deleted theorem MeasurableSpace.comap_not

Modified Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean

Created Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean

added theorem MeasurableEmbedding.comap_eq

added theorem MeasurableEmbedding.comp

added theorem MeasurableEmbedding.exists_measurable_extend

added theorem MeasurableEmbedding.id

added theorem MeasurableEmbedding.iff_comap_eq

added theorem MeasurableEmbedding.measurableSet_image

added theorem MeasurableEmbedding.measurableSet_preimage

added theorem MeasurableEmbedding.measurableSet_range

added theorem MeasurableEmbedding.measurable_comp_iff

added theorem MeasurableEmbedding.measurable_extend

added theorem MeasurableEmbedding.measurable_rangeSplitting

added theorem MeasurableEmbedding.of_measurable_inverse

added theorem MeasurableEmbedding.of_measurable_inverse_on_range

added theorem MeasurableEmbedding.subtype_coe

added structure MeasurableEmbedding

added def MeasurableEquiv.Set.prod

added def MeasurableEquiv.Set.rangeInl

added def MeasurableEquiv.Set.rangeInr

added def MeasurableEquiv.Set.singleton

added def MeasurableEquiv.Set.univ

added def MeasurableEquiv.Simps.apply

added def MeasurableEquiv.Simps.symm_apply

added theorem MeasurableEquiv.apply_symm_apply

added theorem MeasurableEquiv.coe_mk

added theorem MeasurableEquiv.coe_piCongrLeft

added theorem MeasurableEquiv.coe_sumPiEquivProdPi

added theorem MeasurableEquiv.coe_sumPiEquivProdPi_symm

added theorem MeasurableEquiv.coe_toEquiv

added theorem MeasurableEquiv.coe_toEquiv_symm

added theorem MeasurableEquiv.coe_trans

added theorem MeasurableEquiv.eq_image_iff_symm_image_eq

added theorem MeasurableEquiv.ext

added def MeasurableEquiv.finTwoArrow

added def MeasurableEquiv.funUnique

added theorem MeasurableEquiv.image_eq_preimage

added theorem MeasurableEquiv.image_preimage

added theorem MeasurableEquiv.image_symm

added theorem MeasurableEquiv.map_eq

added theorem MeasurableEquiv.measurableSet_image

added theorem MeasurableEquiv.measurableSet_preimage

added def MeasurableEquiv.ofInvolutive

added theorem MeasurableEquiv.ofInvolutive_apply

added theorem MeasurableEquiv.ofInvolutive_symm

added def MeasurableEquiv.ofUniqueOfUnique

added def MeasurableEquiv.piCongrLeft

added theorem MeasurableEquiv.piCongrLeft_apply_apply

added def MeasurableEquiv.piCongrRight

added def MeasurableEquiv.piEquivPiSubtypeProd

added def MeasurableEquiv.piFinSuccAbove

added def MeasurableEquiv.piFinTwo

added def MeasurableEquiv.piFinsetUnion

added def MeasurableEquiv.piMeasurableEquivTProd

added def MeasurableEquiv.piOptionEquivProd

added def MeasurableEquiv.piUnique

added theorem MeasurableEquiv.preimage_image

added theorem MeasurableEquiv.preimage_symm

added def MeasurableEquiv.prodAssoc

added def MeasurableEquiv.prodComm

added def MeasurableEquiv.prodCongr

added def MeasurableEquiv.prodSumDistrib

added def MeasurableEquiv.refl

added theorem MeasurableEquiv.self_comp_symm

added theorem MeasurableEquiv.self_trans_symm

added def MeasurableEquiv.sumCompl

added def MeasurableEquiv.sumCongr

added def MeasurableEquiv.sumPiEquivProdPi

added def MeasurableEquiv.sumProdDistrib

added def MeasurableEquiv.sumProdSum

added def MeasurableEquiv.symm

added theorem MeasurableEquiv.symm_apply_apply

added theorem MeasurableEquiv.symm_bijective

added theorem MeasurableEquiv.symm_comp_self

added theorem MeasurableEquiv.symm_mk

added theorem MeasurableEquiv.symm_preimage_preimage

added theorem MeasurableEquiv.symm_refl

added theorem MeasurableEquiv.symm_symm

added theorem MeasurableEquiv.symm_trans_self

added theorem MeasurableEquiv.toEquiv_injective

added def MeasurableEquiv.trans

added def MeasurableEquiv.ulift.{u,

added structure MeasurableEquiv

added theorem MeasurableSet.exists_measurable_proj

added theorem MeasurableSpace.comap_compl

added theorem MeasurableSpace.comap_not

Created Mathlib/MeasureTheory/MeasurableSpace/Instances.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified scripts/style-exceptions.txt