Commit 2023-05-24 08:50 41490c33

View on Github →

feat: port MeasureTheory.Function.AEEqFun (#4286)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Function/AEEqFun.lean

added theorem ContinuousMap.coeFn_toAEEqFun

added def ContinuousMap.toAEEqFun

added def ContinuousMap.toAEEqFunLinearMap

added def ContinuousMap.toAEEqFunMulHom

added def MeasureTheory.AEEqFun.LiftPred

added def MeasureTheory.AEEqFun.LiftRel

added def MeasureTheory.AEEqFun.cast

added theorem MeasureTheory.AEEqFun.coeFn_abs

added theorem MeasureTheory.AEEqFun.coeFn_comp

added theorem MeasureTheory.AEEqFun.coeFn_compMeasurable

added theorem MeasureTheory.AEEqFun.coeFn_comp₂

added theorem MeasureTheory.AEEqFun.coeFn_comp₂Measurable

added theorem MeasureTheory.AEEqFun.coeFn_const

added theorem MeasureTheory.AEEqFun.coeFn_div

added theorem MeasureTheory.AEEqFun.coeFn_inf

added theorem MeasureTheory.AEEqFun.coeFn_inv

added theorem MeasureTheory.AEEqFun.coeFn_le

added theorem MeasureTheory.AEEqFun.coeFn_mk

added theorem MeasureTheory.AEEqFun.coeFn_mul

added theorem MeasureTheory.AEEqFun.coeFn_one

added theorem MeasureTheory.AEEqFun.coeFn_pair

added theorem MeasureTheory.AEEqFun.coeFn_posPart

added theorem MeasureTheory.AEEqFun.coeFn_pow

added theorem MeasureTheory.AEEqFun.coeFn_smul

added theorem MeasureTheory.AEEqFun.coeFn_sup

added theorem MeasureTheory.AEEqFun.coeFn_zpow

added def MeasureTheory.AEEqFun.comp

added def MeasureTheory.AEEqFun.compMeasurable

added theorem MeasureTheory.AEEqFun.compMeasurable_eq_mk

added theorem MeasureTheory.AEEqFun.compMeasurable_mk

added theorem MeasureTheory.AEEqFun.compMeasurable_toGerm

added theorem MeasureTheory.AEEqFun.comp_eq_mk

added theorem MeasureTheory.AEEqFun.comp_mk

added theorem MeasureTheory.AEEqFun.comp_toGerm

added def MeasureTheory.AEEqFun.comp₂

added def MeasureTheory.AEEqFun.comp₂Measurable

added theorem MeasureTheory.AEEqFun.comp₂Measurable_eq_mk

added theorem MeasureTheory.AEEqFun.comp₂Measurable_eq_pair

added theorem MeasureTheory.AEEqFun.comp₂Measurable_mk_mk

added theorem MeasureTheory.AEEqFun.comp₂Measurable_toGerm

added theorem MeasureTheory.AEEqFun.comp₂_eq_mk

added theorem MeasureTheory.AEEqFun.comp₂_eq_pair

added theorem MeasureTheory.AEEqFun.comp₂_mk_mk

added theorem MeasureTheory.AEEqFun.comp₂_toGerm

added def MeasureTheory.AEEqFun.const

added theorem MeasureTheory.AEEqFun.div_toGerm

added theorem MeasureTheory.AEEqFun.ext

added theorem MeasureTheory.AEEqFun.ext_iff

added theorem MeasureTheory.AEEqFun.induction_on

added theorem MeasureTheory.AEEqFun.induction_on₂

added theorem MeasureTheory.AEEqFun.induction_on₃

added theorem MeasureTheory.AEEqFun.inv_mk

added theorem MeasureTheory.AEEqFun.inv_toGerm

added theorem MeasureTheory.AEEqFun.liftRel_iff_coeFn

added theorem MeasureTheory.AEEqFun.liftRel_mk_mk

added def MeasureTheory.AEEqFun.lintegral

added theorem MeasureTheory.AEEqFun.lintegral_add

added theorem MeasureTheory.AEEqFun.lintegral_coeFn

added theorem MeasureTheory.AEEqFun.lintegral_eq_zero_iff

added theorem MeasureTheory.AEEqFun.lintegral_mk

added theorem MeasureTheory.AEEqFun.lintegral_mono

added def MeasureTheory.AEEqFun.mk

added theorem MeasureTheory.AEEqFun.mk_coeFn

added theorem MeasureTheory.AEEqFun.mk_div

added theorem MeasureTheory.AEEqFun.mk_eq_mk

added theorem MeasureTheory.AEEqFun.mk_le_mk

added theorem MeasureTheory.AEEqFun.mk_mul_mk

added theorem MeasureTheory.AEEqFun.mk_pow

added theorem MeasureTheory.AEEqFun.mk_toGerm

added theorem MeasureTheory.AEEqFun.mk_zpow

added theorem MeasureTheory.AEEqFun.mul_toGerm

added theorem MeasureTheory.AEEqFun.one_def

added theorem MeasureTheory.AEEqFun.one_toGerm

added def MeasureTheory.AEEqFun.pair

added theorem MeasureTheory.AEEqFun.pair_eq_mk

added theorem MeasureTheory.AEEqFun.pair_mk_mk

added def MeasureTheory.AEEqFun.posPart

added theorem MeasureTheory.AEEqFun.posPart_mk

added theorem MeasureTheory.AEEqFun.pow_toGerm

added theorem MeasureTheory.AEEqFun.quot_mk_eq_mk

added theorem MeasureTheory.AEEqFun.smul_mk

added theorem MeasureTheory.AEEqFun.smul_toGerm

added def MeasureTheory.AEEqFun.toGerm

added def MeasureTheory.AEEqFun.toGermMonoidHom

added theorem MeasureTheory.AEEqFun.toGerm_eq

added theorem MeasureTheory.AEEqFun.toGerm_injective

added theorem MeasureTheory.AEEqFun.zpow_toGerm

added def MeasureTheory.AEEqFun

added def MeasureTheory.Measure.aeEqSetoid