Prod

📁 Source: Mathlib/MeasureTheory/Group/Prod.lean

Statistics

Metric	Count
Definitions shearAddRight, shearDivRight, shearMulRight, shearSubRight	4
Theorems absolutelyContinuous_inv, absolutelyContinuous_map_add_right, absolutelyContinuous_map_div_left, absolutelyContinuous_map_mul_right, absolutelyContinuous_map_sub_left, absolutelyContinuous_neg, absolutelyContinuous_of_isAddLeftInvariant, absolutelyContinuous_of_isMulLeftInvariant, ae_measure_preimage_add_right_lt_top, ae_measure_preimage_add_right_lt_top_of_ne_zero, ae_measure_preimage_mul_right_lt_top, ae_measure_preimage_mul_right_lt_top_of_ne_zero, eventuallyConst_inv_set_ae, eventuallyConst_neg_set_ae, inv_absolutelyContinuous, inv_ae, lintegral_lintegral_add_neg, lintegral_lintegral_mul_inv, measurable_measure_add_right, measurable_measure_mul_right, measurePreserving_add_prod, measurePreserving_add_prod_neg, measurePreserving_add_prod_neg_right, measurePreserving_div_prod, measurePreserving_mul_prod, measurePreserving_mul_prod_inv, measurePreserving_mul_prod_inv_right, measurePreserving_prod_add, measurePreserving_prod_add_right, measurePreserving_prod_add_swap, measurePreserving_prod_add_swap_right, measurePreserving_prod_div, measurePreserving_prod_div_swap, measurePreserving_prod_inv_mul, measurePreserving_prod_inv_mul_swap, measurePreserving_prod_mul, measurePreserving_prod_mul_right, measurePreserving_prod_mul_swap, measurePreserving_prod_mul_swap_right, measurePreserving_prod_neg_add, measurePreserving_prod_neg_add_swap, measurePreserving_prod_sub, measurePreserving_prod_sub_swap, measurePreserving_sub_prod, measure_add_lintegral_eq, measure_add_measure_eq, measure_add_right_ne_zero, measure_add_right_null, measure_eq_div_smul, measure_eq_sub_vadd, measure_inv_null, measure_lintegral_div_measure, measure_lintegral_sub_measure, measure_mul_lintegral_eq, measure_mul_measure_eq, measure_mul_right_ne_zero, measure_mul_right_null, measure_neg_null, neg_absolutelyContinuous, neg_ae, quasiMeasurePreserving_add, quasiMeasurePreserving_add_left, quasiMeasurePreserving_add_right, quasiMeasurePreserving_add_swap, quasiMeasurePreserving_div, quasiMeasurePreserving_div_left, quasiMeasurePreserving_div_left_of_right_invariant, quasiMeasurePreserving_div_of_right_invariant, quasiMeasurePreserving_inv, quasiMeasurePreserving_inv_mul, quasiMeasurePreserving_inv_mul_swap, quasiMeasurePreserving_inv_of_right_invariant, quasiMeasurePreserving_mul, quasiMeasurePreserving_mul_left, quasiMeasurePreserving_mul_right, quasiMeasurePreserving_mul_swap, quasiMeasurePreserving_neg, quasiMeasurePreserving_neg_add, quasiMeasurePreserving_neg_add_swap, quasiMeasurePreserving_neg_of_right_invariant, quasiMeasurePreserving_sub, quasiMeasurePreserving_sub_left, quasiMeasurePreserving_sub_left_of_right_invariant, quasiMeasurePreserving_sub_of_right_invariant	84
Total	88

MeasurableEquiv

Definitions

Name	Category	Theorems
shearAddRight 📖	CompOp	—
shearDivRight 📖	CompOp	—
shearMulRight 📖	CompOp	—
shearSubRight 📖	CompOp	—

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
absolutelyContinuous_inv 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.inv_apply
absolutelyContinuous_map_add_right 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.map AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	Measure.map_apply MeasurableAdd.measurable_add_const MeasurableAdd₂.toMeasurableAdd measure_add_right_null
absolutelyContinuous_map_div_left 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.map DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv Measure.map_map MeasurableMul.measurable_const_mul MeasurableMul₂.toMeasurableMul MeasurableInv.measurable_inv map_mul_left_eq_self Measure.AbsolutelyContinuous.map absolutelyContinuous_inv
absolutelyContinuous_map_mul_right 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.map MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Measure.map_apply MeasurableMul.measurable_mul_const MeasurableMul₂.toMeasurableMul measure_mul_right_null
absolutelyContinuous_map_sub_left 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.map SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg Measure.map_map MeasurableAdd.measurable_const_add MeasurableAdd₂.toMeasurableAdd MeasurableNeg.measurable_neg map_add_left_eq_self Measure.AbsolutelyContinuous.map absolutelyContinuous_neg
absolutelyContinuous_neg 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.neg_apply measure_neg_null
absolutelyContinuous_of_isAddLeftInvariant 📖	mathematical	—	Measure.AbsolutelyContinuous	—	measure_add_lintegral_eq measurable_one Iff.not Measure.measure_univ_eq_zero mul_eq_zero ENNReal.instNoZeroDivisors lintegral_zero measure_add_right_null mul_one lintegral_one
absolutelyContinuous_of_isMulLeftInvariant 📖	mathematical	—	Measure.AbsolutelyContinuous	—	measure_mul_lintegral_eq measurable_one Iff.not Measure.measure_univ_eq_zero mul_eq_zero ENNReal.instNoZeroDivisors lintegral_zero measure_mul_right_null mul_one lintegral_one
ae_measure_preimage_add_right_lt_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Top.top instTopENNReal ae Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass ae_of_forall_measure_lt_top_ae_restrict' Measure.neg.instSigmaFinite ae_lt_top measurable_measure_add_right instSFiniteOfSigmaFinite measure_add_lintegral_eq Measurable.indicator measurable_one MeasurableSet.neg lintegral_indicator mul_one Set.indicator_mul_right Set.image_neg_eq_neg Set.indicator_image neg_injective setLIntegral_one ENNReal.mul_ne_top ne_top_of_lt Measure.neg_apply Filter.mp_mem Eq.trans_ne measure_toMeasurable measurableSet_toMeasurable Filter.univ_mem' lt_of_le_of_lt measure_mono Set.preimage_mono subset_toMeasurable
ae_measure_preimage_add_right_lt_top_of_ne_zero 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Top.top instTopENNReal ae Measure.instOuterMeasureClass	—	Filter.Eventually.filter_mono Measure.instOuterMeasureClass Measure.AbsolutelyContinuous.ae_le absolutelyContinuous_of_isAddLeftInvariant instSFiniteOfSigmaFinite Measure.coe_zero Pi.zero_apply ae_measure_preimage_add_right_lt_top
ae_measure_preimage_mul_right_lt_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Top.top instTopENNReal ae Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass ae_of_forall_measure_lt_top_ae_restrict' Measure.inv.instSigmaFinite ae_lt_top measurable_measure_mul_right instSFiniteOfSigmaFinite measure_mul_lintegral_eq Measurable.indicator measurable_one MeasurableSet.inv lintegral_indicator mul_one Set.indicator_mul_right Set.image_inv_eq_inv Set.indicator_image inv_injective setLIntegral_one ENNReal.mul_ne_top ne_top_of_lt Measure.inv_apply Filter.mp_mem Eq.trans_ne measure_toMeasurable measurableSet_toMeasurable Filter.univ_mem' lt_of_le_of_lt measure_mono Set.preimage_mono subset_toMeasurable
ae_measure_preimage_mul_right_lt_top_of_ne_zero 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Top.top instTopENNReal ae Measure.instOuterMeasureClass	—	Filter.Eventually.filter_mono Measure.instOuterMeasureClass Measure.AbsolutelyContinuous.ae_le absolutelyContinuous_of_isMulLeftInvariant instSFiniteOfSigmaFinite Measure.coe_zero Pi.zero_apply ae_measure_preimage_mul_right_lt_top
eventuallyConst_inv_set_ae 📖	mathematical	—	Filter.EventuallyConst Set Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Set.inv_preimage Filter.eventuallyConst_preimage Filter.map_inv inv_ae
eventuallyConst_neg_set_ae 📖	mathematical	—	Filter.EventuallyConst Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Set.neg_preimage Filter.eventuallyConst_preimage Filter.map_neg neg_ae
inv_absolutelyContinuous 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.QuasiMeasurePreserving.absolutelyContinuous quasiMeasurePreserving_inv
inv_ae 📖	mathematical	—	Filter Filter.instInv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	le_antisymm Measure.instOuterMeasureClass Measure.QuasiMeasurePreserving.tendsto_ae quasiMeasurePreserving_inv inv_inv Filter.map_mono
lintegral_lintegral_add_neg 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Prod.instMeasurableSpace Measure.prod	lintegral AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measurable.prodMk Measurable.add measurable_snd measurable_fst Measurable.neg AEMeasurable.comp_quasiMeasurePreserving MeasurePreserving.quasiMeasurePreserving measurePreserving_add_prod_neg lintegral_lintegral MeasurePreserving.map_eq lintegral_map' AEMeasurable.mono' Eq.absolutelyContinuous Measurable.aemeasurable
lintegral_lintegral_mul_inv 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Prod.instMeasurableSpace Measure.prod	lintegral MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measurable.prodMk Measurable.mul measurable_snd measurable_fst Measurable.inv AEMeasurable.comp_quasiMeasurePreserving MeasurePreserving.quasiMeasurePreserving measurePreserving_mul_prod_inv lintegral_lintegral MeasurePreserving.map_eq lintegral_map' AEMeasurable.mono' Eq.absolutelyContinuous Measurable.aemeasurable
measurable_measure_add_right 📖	mathematical	MeasurableSet	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe Measure Set Measure.instFunLike Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	measurable_measure_prodMk_right Measurable.prodMk measurable_const MeasurableAdd₂.measurable_add MeasurableSet.prod MeasurableSet.univ Set.ext Set.mem_preimage Set.mem_prod Set.mem_univ
measurable_measure_mul_right 📖	mathematical	MeasurableSet	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe Measure Set Measure.instFunLike Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	measurable_measure_prodMk_right Measurable.prodMk measurable_const MeasurableMul₂.measurable_mul MeasurableSet.prod MeasurableSet.univ Set.ext
measurePreserving_add_prod 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.comp Measure.measurePreserving_swap measurePreserving_prod_add_swap_right
measurePreserving_add_prod_neg 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	neg_add_rev neg_add_cancel_right MeasurePreserving.comp measurePreserving_prod_neg_add_swap measurePreserving_prod_add_swap
measurePreserving_add_prod_neg_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	sub_add_eq_sub_sub_swap sub_self zero_sub MeasurePreserving.comp measurePreserving_prod_sub_swap measurePreserving_prod_add_swap_right
measurePreserving_div_prod 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace DivInvMonoid.toDiv Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.comp Measure.measurePreserving_swap measurePreserving_prod_div_swap
measurePreserving_mul_prod 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.comp Measure.measurePreserving_swap measurePreserving_prod_mul_swap_right
measurePreserving_mul_prod_inv 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	mul_inv_rev inv_mul_cancel_right MeasurePreserving.comp measurePreserving_prod_inv_mul_swap measurePreserving_prod_mul_swap
measurePreserving_mul_prod_inv_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	div_mul_eq_div_div_swap div_self' one_div MeasurePreserving.comp measurePreserving_prod_div_swap measurePreserving_prod_mul_swap_right
measurePreserving_prod_add 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.skew_product MeasurePreserving.id MeasurableAdd₂.measurable_add Filter.Eventually.of_forall Measure.instOuterMeasureClass map_add_left_eq_self
measurePreserving_prod_add_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.skew_product MeasurePreserving.id Measurable.add measurable_snd measurable_fst Filter.Eventually.of_forall Measure.instOuterMeasureClass map_add_right_eq_self
measurePreserving_prod_add_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_add Measure.measurePreserving_swap
measurePreserving_prod_add_swap_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_add_right Measure.measurePreserving_swap
measurePreserving_prod_div 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace DivInvMonoid.toDiv Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.symm measurePreserving_prod_mul_right
measurePreserving_prod_div_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace DivInvMonoid.toDiv Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_div Measure.measurePreserving_swap
measurePreserving_prod_inv_mul 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	MeasurePreserving.symm measurePreserving_prod_mul
measurePreserving_prod_inv_mul_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_inv_mul Measure.measurePreserving_swap
measurePreserving_prod_mul 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.skew_product MeasurePreserving.id MeasurableMul₂.measurable_mul Filter.Eventually.of_forall Measure.instOuterMeasureClass map_mul_left_eq_self
measurePreserving_prod_mul_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.skew_product MeasurePreserving.id Measurable.mul measurable_snd measurable_fst Filter.Eventually.of_forall Measure.instOuterMeasureClass map_mul_right_eq_self
measurePreserving_prod_mul_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_mul Measure.measurePreserving_swap
measurePreserving_prod_mul_swap_right 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_mul_right Measure.measurePreserving_swap
measurePreserving_prod_neg_add 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	MeasurePreserving.symm measurePreserving_prod_add
measurePreserving_prod_neg_add_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_neg_add Measure.measurePreserving_swap
measurePreserving_prod_sub 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.symm measurePreserving_prod_add_right
measurePreserving_prod_sub_swap 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.comp measurePreserving_prod_sub Measure.measurePreserving_swap
measurePreserving_sub_prod 📖	mathematical	—	MeasurePreserving Prod.instMeasurableSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid Measure.prod	—	MeasurePreserving.comp Measure.measurePreserving_swap measurePreserving_prod_sub_swap
measure_add_lintegral_eq 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike lintegral Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	setLIntegral_one lintegral_indicator lintegral_lintegral_mul Measurable.aemeasurable Measurable.indicator measurable_const lintegral_lintegral_add_neg Measurable.mul ENNReal.instMeasurableMul₂ Measurable.comp measurable_fst measurable_snd MeasurableAdd.measurable_add_const MeasurableAdd₂.toMeasurableAdd Set.indicator_comp_right lintegral_mul_const
measure_add_measure_eq 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike	—	measure_lintegral_sub_measure Measurable.indicator measurable_const setLIntegral_one lintegral_indicator mul_left_comm exists_measurable_superset₂
measure_add_right_ne_zero 📖	—	—	—	—	measure_add_right_null
measure_add_right_null 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instZeroENNReal	—	Set.preimage_preimage neg_add_rev neg_neg measure_neg_null measure_preimage_add MeasurableAdd₂.toMeasurableAdd
measure_eq_div_smul 📖	mathematical	—	ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe Set Measure.instFunLike	—	Measure.ext IsScalarTower.right Measure.smul_apply smul_eq_mul mul_comm mul_div_assoc measure_mul_measure_eq ENNReal.mul_div_cancel
measure_eq_sub_vadd 📖	mathematical	—	ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe Set Measure.instFunLike	—	Measure.ext IsScalarTower.right Measure.smul_apply smul_eq_mul mul_comm mul_div_assoc measure_add_measure_eq ENNReal.mul_div_cancel
measure_inv_null 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instZeroENNReal	—	inv_inv Measure.QuasiMeasurePreserving.preimage_null quasiMeasurePreserving_inv
measure_lintegral_div_measure 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike lintegral DivInvMonoid.toDiv ENNReal.instDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Measurable.div measurableDiv₂_of_mul_inv ENNReal.instMeasurableMul₂ ENNReal.instMeasurableInv Measurable.comp MeasurableInv.measurable_inv measurable_measure_mul_right instSFiniteOfSigmaFinite measure_mul_lintegral_eq inv_inv lintegral_congr_ae Filter.Eventually.mono Measure.instOuterMeasureClass ae_measure_preimage_mul_right_lt_top_of_ne_zero ENNReal.mul_div_cancel measure_mul_right_ne_zero LT.lt.ne
measure_lintegral_sub_measure 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike lintegral DivInvMonoid.toDiv ENNReal.instDivInvMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Set.preimage AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	Measurable.div measurableDiv₂_of_mul_inv ENNReal.instMeasurableMul₂ ENNReal.instMeasurableInv Measurable.comp MeasurableNeg.measurable_neg measurable_measure_add_right instSFiniteOfSigmaFinite measure_add_lintegral_eq neg_neg lintegral_congr_ae Filter.Eventually.mono Measure.instOuterMeasureClass ae_measure_preimage_add_right_lt_top_of_ne_zero ENNReal.mul_div_cancel measure_add_right_ne_zero LT.lt.ne
measure_mul_lintegral_eq 📖	mathematical	MeasurableSet Measurable ENNReal ENNReal.measurableSpace	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike lintegral Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	setLIntegral_one lintegral_indicator lintegral_lintegral_mul Measurable.aemeasurable Measurable.indicator measurable_const lintegral_lintegral_mul_inv Measurable.mul ENNReal.instMeasurableMul₂ Measurable.comp measurable_fst measurable_snd MeasurableMul.measurable_mul_const MeasurableMul₂.toMeasurableMul Set.indicator_comp_right lintegral_mul_const
measure_mul_measure_eq 📖	mathematical	—	ENNReal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike	—	measure_lintegral_div_measure Measurable.indicator measurable_const setLIntegral_one lintegral_indicator mul_left_comm exists_measurable_superset₂
measure_mul_right_ne_zero 📖	—	—	—	—	measure_mul_right_null
measure_mul_right_null 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instZeroENNReal	—	Set.preimage_preimage mul_inv_rev inv_inv measure_inv_null measure_preimage_mul MeasurableMul₂.toMeasurableMul
measure_neg_null 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instZeroENNReal	—	neg_neg Measure.QuasiMeasurePreserving.preimage_null quasiMeasurePreserving_neg
neg_absolutelyContinuous 📖	mathematical	—	Measure.AbsolutelyContinuous Measure.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.QuasiMeasurePreserving.absolutelyContinuous quasiMeasurePreserving_neg
neg_ae 📖	mathematical	—	Filter Filter.instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	le_antisymm Measure.instOuterMeasureClass Measure.QuasiMeasurePreserving.tendsto_ae quasiMeasurePreserving_neg neg_neg Filter.map_mono
quasiMeasurePreserving_add 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_add
quasiMeasurePreserving_add_left 📖	mathematical	—	Measure.QuasiMeasurePreserving AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	Measure.QuasiMeasurePreserving.mono neg_absolutelyContinuous Measure.neg.instSFinite Measure.neg.instIsAddLeftInvariant MeasurableAdd₂.toMeasurableAdd absolutelyContinuous_neg quasiMeasurePreserving_add_right Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_neg_of_right_invariant Measure.neg_neg neg_neg neg_add_rev
quasiMeasurePreserving_add_right 📖	mathematical	—	Measure.QuasiMeasurePreserving AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	MeasurableAdd.measurable_add_const MeasurableAdd₂.toMeasurableAdd Measure.map_apply measure_add_right_null
quasiMeasurePreserving_add_swap 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_add_swap
quasiMeasurePreserving_div 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace DivInvMonoid.toDiv Group.toDivInvMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.mono Measure.AbsolutelyContinuous.prod absolutelyContinuous_inv Measure.AbsolutelyContinuous.rfl inv_absolutelyContinuous quasiMeasurePreserving_div_of_right_invariant Measure.inv.instSFinite Measure.inv.instIsMulRightInvariant MeasurableMul₂.toMeasurableMul
quasiMeasurePreserving_div_left 📖	mathematical	—	Measure.QuasiMeasurePreserving DivInvMonoid.toDiv Group.toDivInvMonoid	—	div_eq_mul_inv Measure.QuasiMeasurePreserving.comp MeasurePreserving.quasiMeasurePreserving measurePreserving_mul_left MeasurableMul₂.toMeasurableMul quasiMeasurePreserving_inv
quasiMeasurePreserving_div_left_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving DivInvMonoid.toDiv Group.toDivInvMonoid	—	Measure.inv_inv Measure.QuasiMeasurePreserving.mono inv_absolutelyContinuous Measure.inv.instSFinite Measure.inv.instIsMulLeftInvariant MeasurableMul₂.toMeasurableMul absolutelyContinuous_inv quasiMeasurePreserving_div_left
quasiMeasurePreserving_div_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace DivInvMonoid.toDiv Group.toDivInvMonoid Measure.prod	—	QuasiMeasurePreserving.prod_of_left MeasurableDiv₂.measurable_div measurableDiv₂_of_mul_inv Filter.Eventually.of_forall Measure.instOuterMeasureClass MeasurePreserving.quasiMeasurePreserving measurePreserving_div_right MeasurableMul₂.toMeasurableMul
quasiMeasurePreserving_inv 📖	mathematical	—	Measure.QuasiMeasurePreserving InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	MeasurableInv.measurable_inv Measure.map_apply Set.inv_preimage Measurable.prodMk Measurable.mul measurable_snd measurable_fst Measurable.inv MeasurableSet.prod MeasurableSet.inv Measure.prod_apply_symm Set.preimage_preimage inv_inv measure_mono_null Measure.instOuterMeasureClass Set.inter_subset_right lintegral_zero MeasurePreserving.map_eq measurePreserving_mul_prod_inv Measure.prod_prod mul_eq_zero ENNReal.instNoZeroDivisors
quasiMeasurePreserving_inv_mul 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_inv_mul
quasiMeasurePreserving_inv_mul_swap 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_inv_mul_swap
quasiMeasurePreserving_inv_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	Measure.inv_inv Measure.QuasiMeasurePreserving.mono inv_absolutelyContinuous Measure.inv.instSFinite Measure.inv.instIsMulLeftInvariant MeasurableMul₂.toMeasurableMul absolutelyContinuous_inv quasiMeasurePreserving_inv
quasiMeasurePreserving_mul 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_mul
quasiMeasurePreserving_mul_left 📖	mathematical	—	Measure.QuasiMeasurePreserving MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	Measure.QuasiMeasurePreserving.mono inv_absolutelyContinuous Measure.inv.instSFinite Measure.inv.instIsMulLeftInvariant MeasurableMul₂.toMeasurableMul absolutelyContinuous_inv quasiMeasurePreserving_mul_right Measure.QuasiMeasurePreserving.comp quasiMeasurePreserving_inv_of_right_invariant Measure.inv_inv inv_inv mul_inv_rev
quasiMeasurePreserving_mul_right 📖	mathematical	—	Measure.QuasiMeasurePreserving MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	—	MeasurableMul.measurable_mul_const MeasurableMul₂.toMeasurableMul Measure.map_apply measure_mul_right_null
quasiMeasurePreserving_mul_swap 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_mul_swap
quasiMeasurePreserving_neg 📖	mathematical	—	Measure.QuasiMeasurePreserving NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	MeasurableNeg.measurable_neg Measure.map_apply Set.neg_preimage Measurable.prodMk Measurable.add measurable_snd measurable_fst Measurable.neg MeasurableSet.prod MeasurableSet.neg Measure.prod_apply_symm Set.preimage_preimage neg_neg measure_mono_null Measure.instOuterMeasureClass Set.inter_subset_right lintegral_zero MeasurePreserving.map_eq measurePreserving_add_prod_neg Measure.prod_prod mul_eq_zero ENNReal.instNoZeroDivisors
quasiMeasurePreserving_neg_add 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_neg_add
quasiMeasurePreserving_neg_add_swap 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.comp Measure.quasiMeasurePreserving_snd MeasurePreserving.quasiMeasurePreserving measurePreserving_prod_neg_add_swap
quasiMeasurePreserving_neg_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	Measure.neg_neg Measure.QuasiMeasurePreserving.mono neg_absolutelyContinuous Measure.neg.instSFinite Measure.neg.instIsAddLeftInvariant MeasurableAdd₂.toMeasurableAdd absolutelyContinuous_neg quasiMeasurePreserving_neg
quasiMeasurePreserving_sub 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid Measure.prod	—	Measure.QuasiMeasurePreserving.mono Measure.AbsolutelyContinuous.prod absolutelyContinuous_neg Measure.AbsolutelyContinuous.rfl neg_absolutelyContinuous quasiMeasurePreserving_sub_of_right_invariant Measure.neg.instSFinite Measure.neg.instIsAddRightInvariant MeasurableAdd₂.toMeasurableAdd
quasiMeasurePreserving_sub_left 📖	mathematical	—	Measure.QuasiMeasurePreserving SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	sub_eq_add_neg Measure.QuasiMeasurePreserving.comp MeasurePreserving.quasiMeasurePreserving measurePreserving_add_left MeasurableAdd₂.toMeasurableAdd quasiMeasurePreserving_neg
quasiMeasurePreserving_sub_left_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving SubNegMonoid.toSub AddGroup.toSubNegMonoid	—	Measure.neg_neg Measure.QuasiMeasurePreserving.mono neg_absolutelyContinuous Measure.neg.instSFinite Measure.neg.instIsAddLeftInvariant MeasurableAdd₂.toMeasurableAdd absolutelyContinuous_neg quasiMeasurePreserving_sub_left
quasiMeasurePreserving_sub_of_right_invariant 📖	mathematical	—	Measure.QuasiMeasurePreserving Prod.instMeasurableSpace SubNegMonoid.toSub AddGroup.toSubNegMonoid Measure.prod	—	QuasiMeasurePreserving.prod_of_left MeasurableSub₂.measurable_sub measurableDiv₂_of_add_neg Filter.Eventually.of_forall Measure.instOuterMeasureClass MeasurePreserving.quasiMeasurePreserving measurePreserving_sub_right MeasurableAdd₂.toMeasurableAdd

---

← Back to Index