FinMeasAdditive

📁 Source: Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean

Statistics

Metric	Count
Definitions DominatedFinMeasAdditive, FinMeasAdditive, setToSimpleFunc	3
Theorems add, add_measure_left, add_measure_right, eq_zero, eq_zero_of_measure_zero, of_measure_le, of_measure_le_smul, of_smul_measure, smul, zero, add, map_empty_eq_zero, map_iUnion_fin_meas_set_eq_sum, of_eq_top_imp_eq_top, of_smul_measure, smul, smul_measure, smul_measure_iff, zero, map_setToSimpleFunc, norm_setToSimpleFunc_le_sum_mul_norm, norm_setToSimpleFunc_le_sum_mul_norm_of_integrable, norm_setToSimpleFunc_le_sum_opNorm, setToSimpleFunc_add, setToSimpleFunc_add_left, setToSimpleFunc_add_left', setToSimpleFunc_congr, setToSimpleFunc_congr', setToSimpleFunc_congr_left, setToSimpleFunc_const, setToSimpleFunc_const', setToSimpleFunc_eq_sum_filter, setToSimpleFunc_indicator, setToSimpleFunc_mono, setToSimpleFunc_mono_left, setToSimpleFunc_mono_left', setToSimpleFunc_neg, setToSimpleFunc_nonneg, setToSimpleFunc_nonneg', setToSimpleFunc_smul, setToSimpleFunc_smul_left, setToSimpleFunc_smul_left', setToSimpleFunc_smul_real, setToSimpleFunc_sub, setToSimpleFunc_zero, setToSimpleFunc_zero', setToSimpleFunc_zero_apply	47
Total	50

MeasureTheory

Definitions

Name	Category	Theorems
DominatedFinMeasAdditive 📖	MathDef	3 math math: dominatedFinMeasAdditive_condExpInd, dominatedFinMeasAdditive_weightedSMul, DominatedFinMeasAdditive.zero
FinMeasAdditive 📖	MathDef	2 math math: FinMeasAdditive.smul_measure_iff, FinMeasAdditive.zero

MeasureTheory.DominatedFinMeasAdditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive	Pi.instAdd Set AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup Real Real.instAdd	—	MeasureTheory.FinMeasAdditive.add Pi.add_apply add_mul Distrib.rightDistribClass LE.le.trans norm_add_le add_le_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add
add_measure_left 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive Real Real.instLE Real.instZero	MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	of_measure_le MeasureTheory.Measure.le_add_left le_rfl
add_measure_right 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive Real Real.instLE Real.instZero	MeasureTheory.Measure MeasureTheory.Measure.instAdd	—	of_measure_le MeasureTheory.Measure.le_add_right le_rfl
eq_zero 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive NormedAddCommGroup.toSeminormedAddCommGroup MeasureTheory.Measure MeasureTheory.Measure.instZero MeasurableSet	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	eq_zero_of_measure_zero
eq_zero_of_measure_zero 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive NormedAddCommGroup.toSeminormedAddCommGroup MeasurableSet DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike instZeroENNReal	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	norm_eq_zero LE.le.antisymm LE.le.trans le_of_eq MeasureTheory.measureReal_def ENNReal.toReal_zero MulZeroClass.mul_zero norm_nonneg
of_measure_le 📖	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder MeasureTheory.DominatedFinMeasAdditive Real Real.instLE Real.instZero	—	—	top_unique Eq.trans_le MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top LE.le.trans_lt mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing ENNReal.toReal_mono LT.lt.ne MeasureTheory.Measure.measure_mono_left
of_measure_le_smul 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder ENNReal MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right MeasureTheory.DominatedFinMeasAdditive Real Real.instLE Real.instZero	Real.instMul ENNReal.toReal	—	IsScalarTower.right of_smul_measure of_measure_le
of_smul_measure 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	Real Real.instMul ENNReal.toReal	—	IsScalarTower.right MeasureTheory.FinMeasAdditive.of_eq_top_imp_eq_top LT.lt.ne LE.le.trans Ne.lt_top smul_eq_mul le_of_eq MeasureTheory.measureReal_ennreal_smul_apply Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul
smul 📖	mathematical	MeasureTheory.DominatedFinMeasAdditive	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup DistribSMul.toSMulZeroClass Real Real.instMul Norm.norm SeminormedAddGroup.toNorm	—	MeasureTheory.FinMeasAdditive.smul LE.le.trans norm_smul_le mul_assoc mul_le_mul IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_rfl norm_nonneg
zero 📖	mathematical	Real Real.instLE Real.instZero	MeasureTheory.DominatedFinMeasAdditive Pi.instZero Set NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SeminormedAddCommGroup.toAddCommGroup	—	MeasureTheory.FinMeasAdditive.zero Pi.zero_apply norm_zero mul_nonneg IsOrderedRing.toPosMulMono Real.instIsOrderedRing ENNReal.toReal_nonneg

MeasureTheory.FinMeasAdditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid	Pi.instAdd Set AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Mathlib.Tactic.Abel.subst_into_add Mathlib.Tactic.Abel.term_atom Mathlib.Tactic.Abel.term_add_const zero_add Mathlib.Tactic.Abel.const_add_term
map_empty_eq_zero 📖	mathematical	MeasureTheory.FinMeasAdditive AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid	Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	LT.lt.ne LE.le.trans_lt Eq.le MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.coe_lt_top add_left_cancel AddLeftCancelSemigroup.toIsLeftCancelAdd add_zero Set.union_empty MeasurableSet.empty Set.disjoint_empty
map_iUnion_fin_meas_set_eq_sum 📖	mathematical	Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid MeasureTheory.FinMeasAdditive MeasurableSet Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	Set.iUnion Finset Finset.instMembership Finset.sum	—	Finset.induction_on instIsEmptyFalse Set.iUnion_congr_Prop Set.iUnion_false Set.iUnion_empty Finset.sum_insert Finset.mem_insert_of_mem Finset.measurableSet_biUnion Finset.mem_insert_self LT.lt.ne MeasureTheory.measure_biUnion_lt_top Finset.finite_toSet Ne.lt_top Finset.iSup_insert
of_eq_top_imp_eq_top 📖	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike Top.top instTopENNReal MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid	—	—	—
of_smul_measure 📖	—	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	—	IsScalarTower.right of_eq_top_imp_eq_top ENNReal.mul_eq_top smul_eq_mul MeasureTheory.Measure.smul_apply
smul 📖	mathematical	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass	—	smul_add
smul_measure 📖	mathematical	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid	ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	of_eq_top_imp_eq_top IsScalarTower.right MeasureTheory.Measure.smul_apply smul_eq_mul ENNReal.mul_eq_top
smul_measure_iff 📖	mathematical	—	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid ENNReal MeasureTheory.Measure MeasureTheory.Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right of_smul_measure smul_measure
zero 📖	mathematical	—	MeasureTheory.FinMeasAdditive AddCommMonoid.toAddMonoid Pi.instZero Set AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	add_zero

MeasureTheory.SimpleFunc

Definitions

Name	Category	Theorems
setToSimpleFunc 📖	CompOp	31 math math: setToSimpleFunc_congr', setToSimpleFunc_smul_left, setToSimpleFunc_mono_left, setToSimpleFunc_nonneg, setToSimpleFunc_zero', setToSimpleFunc_const, setToSimpleFunc_zero_apply, setToSimpleFunc_congr_left, setToSimpleFunc_add_left, setToSimpleFunc_smul_left', setToSimpleFunc_add_left', MeasureTheory.L1.SimpleFunc.setToL1S_eq_setToSimpleFunc, setToSimpleFunc_sub, setToSimpleFunc_add, norm_setToSimpleFunc_le_sum_mul_norm, norm_setToSimpleFunc_le_sum_opNorm, setToSimpleFunc_neg, setToSimpleFunc_smul, setToSimpleFunc_indicator, integral_def, setToSimpleFunc_zero, setToSimpleFunc_congr, setToSimpleFunc_eq_sum_filter, setToSimpleFunc_mono, norm_setToSimpleFunc_le_sum_mul_norm_of_integrable, setToSimpleFunc_const', norm_setToSimpleFunc_le_integral_norm, setToSimpleFunc_smul_real, setToSimpleFunc_mono_left', setToSimpleFunc_nonneg', map_setToSimpleFunc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_setToSimpleFunc 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	setToSimpleFunc map Finset.sum range ContinuousLinearMap.funLike Set.preimage Set Set.instSingletonSet	—	RingHomIsometric.ids MeasureTheory.FinMeasAdditive.map_empty_eq_zero LT.lt.ne measure_preimage_lt_top_of_integrable Finset.sum_congr range_map Finset.sum_image' mem_range Finset.filter.congr_simp map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Finset.sum_eq_zero Finset.mem_filter map_preimage_singleton Finset.set_biUnion_preimage_singleton IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.FinMeasAdditive.map_iUnion_fin_meas_set_eq_sum measurableSet_fiber ContinuousLinearMap.coe_sum' Finset.sum_apply
norm_setToSimpleFunc_le_sum_mul_norm 📖	mathematical	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instMul MeasureTheory.Measure.real	NormedAddCommGroup.toNorm setToSimpleFunc Finset.sum Real.instAddCommMonoid range Set.preimage DFunLike.coe MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	norm_setToSimpleFunc_le_sum_opNorm Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing measurableSet_fiber norm_nonneg Finset.mul_sum Finset.sum_congr le_refl
norm_setToSimpleFunc_le_sum_mul_norm_of_integrable 📖	mathematical	Real Real.instLE Norm.norm ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Real.instMul MeasureTheory.Measure.real MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	NormedAddCommGroup.toNorm setToSimpleFunc Finset.sum Real.instAddCommMonoid range Set.preimage Set Set.instSingletonSet	—	norm_setToSimpleFunc_le_sum_opNorm Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid eq_or_ne norm_zero MulZeroClass.mul_zero mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing measurableSet_fiber measure_preimage_lt_top_of_integrable le_of_lt norm_pos_iff Finset.mul_sum Finset.sum_congr le_refl
norm_setToSimpleFunc_le_sum_opNorm 📖	mathematical	—	Real Real.instLE Norm.norm NormedAddCommGroup.toNorm setToSimpleFunc Finset.sum Real.instAddCommMonoid range Real.instMul ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.hasOpNorm DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField Set.preimage DFunLike.coe MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	norm_sum_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid ContinuousLinearMap.le_opNorm RingHomIsometric.ids
setToSimpleFunc_add 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc instAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomIsometric.ids integrable_pair add_eq_map₂ map_setToSimpleFunc add_zero Finset.sum_congr ContinuousLinearMap.map_add Finset.sum_add_distrib Prod.snd_zero Prod.fst_zero
setToSimpleFunc_add_left 📖	mathematical	—	setToSimpleFunc Pi.instAdd Set ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup Finset.sum_congr Finset.sum_add_distrib
setToSimpleFunc_add_left' 📖	mathematical	ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup SeminormedAddCommGroup.toIsTopologicalAddGroup MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	IsTopologicalAddGroup.toContinuousAdd SeminormedAddCommGroup.toIsTopologicalAddGroup setToSimpleFunc_eq_sum_filter measurableSet_preimage measure_preimage_lt_top_of_integrable Finset.mem_filter Finset.sum_add_distrib Finset.sum_congr Pi.add_apply
setToSimpleFunc_congr 📖	mathematical	ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero MeasureTheory.FinMeasAdditive ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	setToSimpleFunc	—	RingHomIsometric.ids MeasureTheory.Measure.instOuterMeasureClass setToSimpleFunc_congr' MeasureTheory.integrable_congr MeasurableSet.inter measurableSet_fiber MeasureTheory.measure_mono_null MeasureTheory.ae_iff Filter.EventuallyEq.eq_1
setToSimpleFunc_congr' 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike Pairwise Set Set.instInter Set.preimage Set.instSingletonSet ContinuousLinearMap.zero	setToSimpleFunc	—	RingHomIsometric.ids integrable_pair map_setToSimpleFunc Prod.fst_zero Prod.snd_zero Finset.sum_congr mem_range pair_preimage_singleton
setToSimpleFunc_congr_left 📖	mathematical	MeasureTheory.Integrable UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc	—	Finset.sum_congr map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass measurableSet_fiber measure_preimage_lt_top_of_integrable
setToSimpleFunc_const 📖	mathematical	Set Set.instEmptyCollection ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero	setToSimpleFunc const DFunLike.coe ContinuousLinearMap.funLike Set.univ	—	isEmpty_or_nonempty Unique.instSubsingleton Finset.sum_congr range_eq_empty_of_isEmpty setToSimpleFunc_const'
setToSimpleFunc_const' 📖	mathematical	—	setToSimpleFunc const DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike Set.univ	—	Finset.sum_congr range_const Finset.sum_singleton Set.preimage_const_of_mem
setToSimpleFunc_eq_sum_filter 📖	mathematical	—	setToSimpleFunc Finset.sum ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Finset.filter NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup range DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike Set.preimage MeasureTheory.SimpleFunc instFunLike Set Set.instSingletonSet	—	Finset.sum_filter_of_ne map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
setToSimpleFunc_indicator 📖	mathematical	Set Set.instEmptyCollection ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero MeasurableSet	setToSimpleFunc piecewise const NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe ContinuousLinearMap.funLike	—	Set.eq_empty_or_nonempty piecewise_empty setToSimpleFunc_zero_apply eq_or_ne Finset.sum_congr piecewise_univ range_const Set.Nonempty.to_type Finset.sum_singleton Set.preimage_const_of_mem range_indicator piecewise.congr_simp Finset.insert_eq_of_mem piecewise_same map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Finset.sum_insert Finset.mem_singleton ContinuousLinearMap.map_zero add_zero Set.piecewise_eq_indicator Set.indicator_preimage Function.const_def Set.mem_singleton Function.const_zero Set.preimage_const_of_notMem Set.mem_singleton_iff Set.ite_empty_right Set.univ_inter
setToSimpleFunc_mono 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe ContinuousLinearMap.funLike MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.SimpleFunc instFunLike instLE	setToSimpleFunc	—	RingHomIsometric.ids sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono setToSimpleFunc_sub setToSimpleFunc_nonneg' MeasureTheory.Integrable.sub
setToSimpleFunc_mono_left 📖	mathematical	Preorder.toLE PartialOrder.toPreorder DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike	setToSimpleFunc	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono
setToSimpleFunc_mono_left' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc	—	Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass measurableSet_fiber measure_preimage_lt_top_of_integrable
setToSimpleFunc_neg 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc instNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	RingHomIsometric.ids map_setToSimpleFunc neg_zero setToSimpleFunc.eq_1 Finset.sum_neg_distrib Finset.sum_congr map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass
setToSimpleFunc_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike MeasureTheory.SimpleFunc instLE instZero	setToSimpleFunc	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono Set.mem_range mem_range le_trans
setToSimpleFunc_nonneg' 📖	mathematical	Preorder.toLE PartialOrder.toPreorder NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup DFunLike.coe ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.funLike MeasureTheory.SimpleFunc instLE instZero MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup instFunLike	setToSimpleFunc	—	Finset.sum_nonneg IsOrderedAddMonoid.toAddLeftMono map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass measurableSet_fiber measure_preimage_lt_top_of_integrable Set.mem_range mem_range
setToSimpleFunc_smul 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid DFunLike.coe ContinuousLinearMap.funLike SMulZeroClass.toSMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc instSMul	—	RingHomIsometric.ids smul_eq_map map_setToSimpleFunc smul_zero Finset.sum_congr Finset.smul_sum
setToSimpleFunc_smul_left 📖	mathematical	—	setToSimpleFunc Real ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul Finset.sum_congr Finset.smul_sum
setToSimpleFunc_smul_left' 📖	mathematical	Real ContinuousLinearMap Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.instSMul DistribMulAction.toDistribSMul Real.instMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self Real.instCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing Real.commRing UniformContinuousConstSMul.to_continuousConstSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass IsBoundedSMul.toUniformContinuousConstSMul Real.pseudoMetricSpace Real.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup NormedSpace.toIsBoundedSMul MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc ESeminormedAddMonoid.toAddMonoid ESeminormedAddCommMonoid.toESeminormedAddMonoid	—	smulCommClass_self UniformContinuousConstSMul.to_continuousConstSMul IsBoundedSMul.toUniformContinuousConstSMul NormedSpace.toIsBoundedSMul setToSimpleFunc_eq_sum_filter measurableSet_preimage measure_preimage_lt_top_of_integrable Finset.mem_filter Finset.smul_sum Finset.sum_congr ContinuousLinearMap.smul_apply
setToSimpleFunc_smul_real 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Real.instMonoid Module.toDistribMulAction	—	RingHomIsometric.ids smul_eq_map map_setToSimpleFunc smul_zero Finset.sum_congr map_smul SemilinearMapClass.toMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass Finset.smul_sum
setToSimpleFunc_sub 📖	mathematical	MeasureTheory.FinMeasAdditive ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ESeminormedAddMonoid.toAddMonoid ContinuousLinearMap.toNormedAddCommGroup DenselyNormedField.toNontriviallyNormedField Real.denselyNormedField RingHomIsometric.ids SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Real.normedCommRing ESeminormedAddCommMonoid.toESeminormedAddMonoid MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup	—	RingHomIsometric.ids sub_eq_add_neg setToSimpleFunc_add integrable_iff coe_neg Pi.neg_def Set.preimage_comp Set.neg_preimage Set.neg_singleton setToSimpleFunc_neg
setToSimpleFunc_zero 📖	mathematical	—	setToSimpleFunc Pi.instZero Set ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Finset.sum_congr Finset.sum_const_zero
setToSimpleFunc_zero' 📖	mathematical	ContinuousLinearMap Real Real.semiring RingHom.id Semiring.toNonAssocSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule Real.normedField ContinuousLinearMap.zero MeasureTheory.Integrable SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup DFunLike.coe MeasureTheory.SimpleFunc instFunLike	setToSimpleFunc NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	Finset.sum_eq_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass measurableSet_fiber measure_preimage_lt_top_of_integrable ContinuousLinearMap.zero_apply
setToSimpleFunc_zero_apply 📖	mathematical	—	setToSimpleFunc MeasureTheory.SimpleFunc instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NormedAddCommGroup.toAddCommGroup	—	isEmpty_or_nonempty Finset.sum_congr range_eq_empty_of_isEmpty range_zero Finset.sum_singleton map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass ContinuousSemilinearMapClass.toSemilinearMapClass ContinuousLinearMap.continuousSemilinearMapClass

---

← Back to Index