SimpleFunc

📁 Source: Mathlib/MeasureTheory/Function/SimpleFunc.lean

Statistics

Metric	Count
Definitions `SimpleFunc`, `FinMeasSupp`, `approx`, `bind`, `comp`, `const`, `eapprox`, `eapproxDiff`, `ennrealRatEmbed`, `extend`, `hasIntPow`, `hasNatPow`, `hasNatSMul`, `instAdd`, `instAddCommGroup`, `instAddCommMonoid`, `instAddGroup`, `instAddMonoid`, `instAlgebra`, `instBoundedOrder`, `instCommGroup`, `instCommMonoid`, `instCommRing`, `instCommSemiring`, `instDiv`, `instFunLike`, `instGroup`, `instInf`, `instInhabited`, `instIntCast`, `instInv`, `instInvolutiveStar`, `instLE`, `instLattice`, `instModule`, `instMonoid`, `instMul`, `instMulAction`, `instNatCast`, `instNeg`, `instNonAssocRing`, `instNonAssocSemiring`, `instNonUnitalCommRing`, `instNonUnitalCommSemiring`, `instNonUnitalNonAssocSemiring`, `instNonUnitalRing`, `instNonUnitalSemiring`, `instOne`, `instOrderBot`, `instOrderTop`, `instPartialOrder`, `instPreorder`, `instRing`, `instSMul`, `instSemilatticeInf`, `instSemilatticeSup`, `instSemiring`, `instStar`, `instStarAddMonoid`, `instStarMul`, `instStarRing`, `instSub`, `instSup`, `instVAdd`, `instZero`, `lintegral`, `lintegralₗ`, `map`, `ofFinite`, `ofIsEmpty`, `pair`, `piecewise`, `range`, `restrict`, `seq`, `toFun`	76
Theorems `add_simpleFunc`, `ennreal_induction`, `ennreal_sigmaFinite_induction`, `simpleFunc_add`, `add`, `iff_lintegral_lt_top`, `lintegral_lt_top`, `map`, `map_iff`, `map₂`, `meas_preimage_singleton_ne_zero`, `mul`, `of_lintegral_ne_top`, `of_map`, `pair`, `add_apply`, `add_eq_map₂`, `add_lintegral`, `aemeasurable`, `apply_mk`, `approx_apply`, `approx_comp`, `bind_apply`, `bind_const`, `coe_add`, `coe_algebraMap`, `coe_comp`, `coe_const`, `coe_div`, `coe_inf`, `coe_injective`, `coe_intCast`, `coe_inv`, `coe_le`, `coe_le_coe`, `coe_lt_coe`, `coe_map`, `coe_mk`, `coe_mul`, `coe_natCast`, `coe_neg`, `coe_one`, `coe_piecewise`, `coe_pow`, `coe_range`, `coe_restrict`, `coe_smul`, `coe_star`, `coe_sub`, `coe_sup`, `coe_vadd`, `coe_zero`, `coe_zpow`, `const_add_eq_map`, `const_algebraMap`, `const_apply`, `const_lintegral`, `const_lintegral_restrict`, `const_mul_eq_map`, `const_mul_lintegral`, `const_one`, `const_zero`, `div_apply`, `eapprox_comp`, `eapprox_lt_top`, `ennrealRatEmbed_encode`, `eq_zero_of_mem_range_zero`, `exists_forall_le`, `exists_range_iff`, `ext`, `ext_iff`, `extend_apply`, `extend_apply'`, `extend_comp_eq`, `extend_comp_eq'`, `finMeasSupp_iff`, `finMeasSupp_iff_support`, `finite_range`, `finite_range'`, `finset_sup_apply`, `forall_mem_range`, `iSup_approx_apply`, `iSup_coe_eapprox`, `iSup_eapprox_apply`, `induction`, `induction'`, `inf_apply`, `instIsOrderedAddMonoid`, `instIsOrderedMonoid`, `instIsScalarTower`, `instSMulCommClass`, `inv_apply`, `le_sup_lintegral`, `lintegral_add`, `lintegral_congr`, `lintegral_eq_of_measure_preimage`, `lintegral_eq_of_subset`, `lintegral_eq_of_subset'`, `lintegral_finset_sum`, `lintegral_map`, `lintegral_map'`, `lintegral_mono`, `lintegral_mono_fun`, `lintegral_mono_measure`, `lintegral_restrict`, `lintegral_restrict_iUnion_of_directed`, `lintegral_smul`, `lintegral_sum`, `lintegral_zero`, `map_add`, `map_apply`, `map_coe_ennreal_restrict`, `map_coe_nnreal_restrict`, `map_const`, `map_fst_pair`, `map_lintegral`, `map_map`, `map_mul`, `map_preimage`, `map_preimage_singleton`, `map_restrict_of_zero`, `map_snd_pair`, `measurable`, `measurableSet_cut`, `measurableSet_fiber`, `measurableSet_fiber'`, `measurableSet_preimage`, `measurableSet_support`, `measurable_bind`, `measure_support_lt_top`, `measure_support_lt_top_of_lintegral_ne_top`, `mem_image_of_mem_range_restrict`, `mem_range`, `mem_range_of_measure_ne_zero`, `mem_range_self`, `mem_restrict_range`, `mk_le_mk`, `mk_lt_mk`, `monotone_approx`, `monotone_eapprox`, `mul_apply`, `mul_eq_map₂`, `neg_apply`, `pair_apply`, `pair_preimage`, `pair_preimage_singleton`, `piecewise_apply`, `piecewise_compl`, `piecewise_empty`, `piecewise_mono`, `piecewise_same`, `piecewise_univ`, `pow_apply`, `preimage_eq_empty_iff`, `range_comp_subset_range`, `range_const`, `range_const_subset`, `range_eq_empty_of_isEmpty`, `range_indicator`, `range_map`, `range_one`, `range_zero`, `restrict_apply`, `restrict_const_lintegral`, `restrict_empty`, `restrict_lintegral`, `restrict_lintegral_eq_lintegral_restrict`, `restrict_mono`, `restrict_of_not_measurable`, `restrict_preimage`, `restrict_preimage_singleton`, `restrict_univ`, `seq_apply`, `simpleFunc_bot`, `simpleFunc_bot'`, `smul_apply`, `smul_const`, `smul_eq_map`, `sub_apply`, `sum_eapproxDiff`, `sum_measure_preimage_singleton`, `sum_range_measure_preimage_singleton`, `sup_apply`, `sup_eq_map₂`, `support_eq`, `support_indicator`, `tendsto_eapprox`, `tsum_eapproxDiff`, `vadd_apply`, `zero_lintegral`, `zpow_apply`	191
Total	267

Measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_simpleFunc` 📖	mathematical	`Measurable`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike`	—	`MeasureTheory.SimpleFunc.induction` `Set.piecewise_same` `Set.piecewise_add` `piecewise` `add_const` `Set.piecewise_eq_of_mem` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Set.disjoint_left` `Set.piecewise_eq_of_notMem` `AddRightCancelSemigroup.toIsRightCancelAdd` `MeasureTheory.SimpleFunc.measurableSet_support`
`ennreal_induction` 📖	—	`Set.indicator` `ENNReal` `instZeroENNReal` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Measurable` `ENNReal.measurableSpace`	—	—	`MeasureTheory.SimpleFunc.iSup_eapprox_apply` `MeasureTheory.SimpleFunc.measurable` `MeasureTheory.SimpleFunc.monotone_eapprox` `MeasureTheory.SimpleFunc.induction`
`ennreal_sigmaFinite_induction` 📖	—	`Set.indicator` `ENNReal` `instZeroENNReal` `Pi.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `Measurable` `ENNReal.measurableSpace`	—	—	`ennreal_induction` `Set.indicator_iUnion_apply` `MeasureTheory.iUnion_spanningSets` `Set.inter_univ` `indicator` `measurable_const` `MeasurableSet.inter` `MeasureTheory.measurableSet_spanningSets` `le_imp_le_of_le_of_le` `Set.indicator_le_indicator_apply_of_subset` `Set.inter_subset_inter` `subset_refl` `Set.instReflSubset` `MeasureTheory.spanningSets_mono` `zero_le` `ENNReal.instCanonicallyOrderedAdd` `le_refl` `MeasureTheory.measure_inter_lt_top_of_right_ne_top` `LT.lt.ne` `MeasureTheory.measure_spanningSets_lt_top`
`simpleFunc_add` 📖	mathematical	`Measurable`	`Pi.instAdd` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddRightCancelMonoid.toAddMonoid` `AddCancelMonoid.toAddRightCancelMonoid` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike`	—	`MeasureTheory.SimpleFunc.induction` `Set.piecewise_same` `Set.piecewise_add` `piecewise` `const_add` `Set.piecewise_eq_of_mem` `AddRightCancelSemigroup.toIsRightCancelAdd` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `Set.disjoint_left` `Set.piecewise_eq_of_notMem` `MeasureTheory.SimpleFunc.measurableSet_support`

MeasureTheory

Definitions

Name	Category	Theorems
`SimpleFunc` 📖	CompData	221 math, 2 bridge math: `SimpleFunc.coe_range`, `SimpleFunc.exists_forall_le`, `SimpleFunc.posPart_sub_negPart`, `lintegral_def`, `SimpleFunc.sum_measure_preimage_singleton`, `SimpleFunc.integral_piecewise_zero`, `SimpleFunc.coe_zpow`, `SimpleFunc.coe_lt_coe`, `Lp.simpleFunc.toSimpleFunc_indicatorConst`, `MemLp.exists_simpleFunc_eLpNorm_sub_lt`, `StronglyMeasurable.tendsto_approxBounded_ae`, `SimpleFunc.forall_mem_range`, `Measurable.add_simpleFunc`, `SimpleFunc.coe_sup`, `Integrable.simpleFunc_mul'`, `SimpleFunc.tendsto_approxOn_range_L1_enorm`, `measure_support_eapprox_lt_top`, `SimpleFunc.nearestPtInd_succ`, `SimpleFunc.const_apply`, `SimpleFunc.map_mul`, `SimpleFunc.measurable_bind`, `SimpleFunc.memLp_zero`, `SimpleFunc.instIsOrderedAddMonoid`, `SimpleFunc.apply_mk`, `FinStronglyMeasurable.tendsto_approx`, `Integrable.simpleFunc_mul`, `SimpleFunc.piecewise_apply`, `SimpleFunc.iSup_coe_eapprox`, `SimpleFunc.restrict_lintegral`, `SimpleFunc.integral_eq_sum_filter`, `SimpleFunc.mem_range`, `SimpleFunc.const_add_eq_map`, `SimpleFunc.setToSimpleFunc_zero_apply`, `SimpleFunc.coe_add`, `SimpleFunc.memLp_iff_integrable`, `Lp.simpleFunc.stronglyMeasurable`, `Lp.simpleFunc.sub_toSimpleFunc`, `SimpleFunc.mul_eq_map₂`, `SimpleFunc.tendsto_eapprox`, `SimpleFunc.finite_range`, `Lp.simpleFunc.smul_toSimpleFunc`, `SimpleFunc.coe_piecewise`, `SimpleFunc.coe_star`, `SimpleFunc.coe_le`, `SimpleFunc.nnnorm_approxOn_le`, `SimpleFunc.exists_forall_norm_le`, `SimpleFunc.map_add`, `SimpleFunc.pair_preimage_singleton`, `SimpleFunc.preimage_eq_empty_iff`, `SimpleFunc.measurable`, `SimpleFunc.coe_zero`, `SimpleFunc.memLp_iff_finMeasSupp`, `exists_simpleFunc_forall_lintegral_sub_lt_of_pos`, `SimpleFunc.lintegral_restrict`, `condExp_stronglyMeasurable_simpleFunc_mul`, `Lp.simpleFunc.add_toSimpleFunc`, `SimpleFunc.norm_approxOn_y₀_le`, `SimpleFunc.le_sup_lintegral`, `SimpleFunc.eapprox_comp`, `SimpleFunc.nearestPtInd_le`, `SimpleFunc.map_lintegral`, `SimpleFunc.coe_mul`, `SimpleFunc.memLp_approxOn_range`, `SimpleFunc.mk_le_mk`, `SimpleFunc.memLp_iff`, `tendsto_setToFun_approxOn_of_measurable_of_range_subset`, `SimpleFunc.edist_approxOn_y0_le`, `SimpleFunc.norm_setToSimpleFunc_le_sum_mul_norm`, `SimpleFunc.coe_map`, `SimpleFunc.const_one`, `SimpleFunc.edist_approxOn_mono`, `condExp_stronglyMeasurable_simpleFunc_bilin`, `SimpleFunc.approxOn_mem`, `SimpleFunc.sum_eapproxDiff`, `SimpleFunc.support_indicator`, `SimpleFunc.coe_pow`, `SimpleFunc.coe_natCast`, `SimpleFunc.range_zero`, `L1.SimpleFunc.norm_eq_sum_mul`, `SimpleFunc.exists_range_iff`, `SimpleFunc.lintegral_eq_of_subset'`, `SimpleFunc.norm_setToSimpleFunc_le_sum_opNorm`, `SimpleFunc.FinMeasSupp.mul`, `SimpleFunc.FinMeasSupp.integrable`, `SimpleFunc.pair_preimage`, `exists_lt_lintegral_simpleFunc_of_lt_lintegral`, `SimpleFunc.coe_toLargerSpace_eq`, `SimpleFunc.vadd_apply`, `SimpleFunc.FinMeasSupp.meas_preimage_singleton_ne_zero`, `SimpleFunc.memLp_top`, `SimpleFunc.coe_vadd`, `SimpleFunc.integrable_iff`, `SimpleFunc.neg_apply`, `SimpleFunc.tendsto_approxOn`, `SimpleFunc.const_mul_eq_map`, `SimpleFunc.add_lintegral`, `SimpleFunc.inv_apply`, `Lp.simpleFunc.neg_toSimpleFunc`, `SimpleFunc.ext_iff`, `L1.SimpleFunc.integrable`, `SimpleFunc.coe_le_coe`, `Lp.simpleFunc.memLp`, `Lp.simpleFunc.norm_toSimpleFunc`, `L1.SimpleFunc.negPart_toSimpleFunc`, `SimpleFunc.measurableSet_support`, `SimpleFunc.memLp_approxOn`, `SimpleFunc.restrict_empty`, `SimpleFunc.monotone_eapprox`, `Measurable.simpleFunc_add`, `SimpleFunc.coe_smul`, `Lp.simpleFunc.toLp_zero`, `SimpleFunc.bind_apply`, `L1.SimpleFunc.posPart_toSimpleFunc`, `SimpleFunc.sup_apply`, `lintegral_eq_nnreal`, `SimpleFunc.measure_support_lt_top_of_lintegral_ne_top`, `SimpleFunc.coe_mk`, `SimpleFunc.coe_neg`, `SimpleFunc.integrable_approxOn_range`, `SimpleFunc.exists_le_lowerSemicontinuous_lintegral_ge`, `SimpleFunc.div_apply`, `SimpleFunc.coe_sub`, `SimpleFunc.coe_restrict`, `SimpleFunc.integral_eq_sum_of_subset`, `SimpleFunc.restrict_of_not_measurable`, `SimpleFunc.seq_apply`, `SimpleFunc.mem_restrict_range`, `SimpleFunc.eLpNorm'_eq`, `SimpleFunc.measurableSet_preimage`, `SimpleFunc.const_algebraMap`, `Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq`, `SimpleFunc.tendsto_nearestPt`, `SimpleFunc.memLp_of_isFiniteMeasure`, `SimpleFunc.smul_eq_map`, `SimpleFunc.coe_comp`, `SimpleFunc.sub_apply`, `SimpleFunc.range_one`, `SimpleFunc.integrable_approxOn`, `SimpleFunc.pair_apply`, `StronglyMeasurable.tendsto_approx`, `SimpleFunc.integrable_of_isFiniteMeasure`, `SimpleFunc.coe_div`, `SimpleFunc.measurableSet_fiber`, `SimpleFunc.pow_apply`, `SimpleFunc.restrict_apply`, `SimpleFunc.smul_const`, `SimpleFunc.stronglyMeasurable`, `SimpleFunc.coe_inf`, `SimpleFunc.setToSimpleFunc_eq_sum_filter`, `SimpleFunc.simpleFunc_bot`, `SimpleFunc.norm_approxOn_zero_le`, `SimpleFunc.aemeasurable`, `SimpleFunc.const_mul_lintegral`, `SimpleFunc.iSup_eapprox_apply`, `SimpleFunc.zpow_apply`, `Lp.simpleFunc.aestronglyMeasurable`, `ProbabilityTheory.strong_law_ae_simpleFunc_comp`, `SimpleFunc.mem_image_of_mem_range_restrict`, `SimpleFunc.exists_upperSemicontinuous_le_lintegral_le`, `SimpleFunc.aestronglyMeasurable`, `SimpleFunc.measurableSet_cut`, `SimpleFunc.coe_intCast`, `Lp.simpleFunc.measurable`, `SimpleFunc.mk_lt_mk`, `StronglyMeasurable.stronglyMeasurable_in_set`, `SimpleFunc.integrable_iff_finMeasSupp`, `HasCompactSupport.exists_simpleFunc_approx_of_prod`, `SimpleFunc.integral_eq`, `tendsto_setToFun_approxOn_of_measurable`, `SimpleFunc.extend_apply'`, `SimpleFunc.tsum_eapproxDiff`, `SimpleFunc.iSup_approx_apply`, `SimpleFunc.const_zero`, `FinStronglyMeasurable.fin_support_approx`, `SimpleFunc.map_apply`, `SimpleFunc.eapprox_lt_top`, `SimpleFunc.inf_apply`, `SimpleFunc.mem_range_self`, `SimpleFunc.FinMeasSupp.add`, `SimpleFunc.support_eq`, `SimpleFunc.tendsto_approxOn_L1_enorm`, `SimpleFunc.approx_comp`, `SimpleFunc.instIsScalarTower`, `SimpleFunc.edist_nearestPt_le`, `SimpleFunc.restrict_preimage`, `SimpleFunc.approx_apply`, `SimpleFunc.coe_one`, `SimpleFunc.finMeasSupp_iff`, `SimpleFunc.finset_sup_apply`, `SimpleFunc.map_preimage`, `tendsto_integral_norm_approxOn_sub`, `SimpleFunc.sup_eq_map₂`, `SimpleFunc.edist_approxOn_le`, `SimpleFunc.add_eq_map₂`, `Lp.simpleFunc.toSimpleFunc_eq_toFun`, `SimpleFunc.coe_algebraMap`, `SimpleFunc.coe_const`, `SimpleFunc.coe_inv`, `SimpleFunc.smul_apply`, `SimpleFunc.tendsto_approxOn_range_Lp`, `SimpleFunc.monotone_approx`, `SimpleFunc.extend_comp_eq'`, `SimpleFunc.add_apply`, `StronglyMeasurable.norm_approxBounded_le`, `Lp.simpleFunc.aemeasurable`, `SimpleFunc.mul_apply`, `SimpleFunc.tendsto_approxOn_Lp_eLpNorm`, `SimpleFunc.approxOn_zero`, `StronglyMeasurable.tendsto_approxBounded_of_norm_le`, `SimpleFunc.extend_apply`, `SimpleFunc.restrict_preimage_singleton`, `SimpleFunc.finMeasSupp_iff_support`, `SimpleFunc.lintegral_eq_lintegral`, `Lp.simpleFunc.zero_toSimpleFunc`, `SimpleFunc.zero_lintegral`, `SimpleFunc.instSMulCommClass`, `SimpleFunc.tendsto_approxOn_range_Lp_eLpNorm`, `SimpleFunc.instIsOrderedMonoid`, `SimpleFunc.map_preimage_singleton`, `SimpleFunc.sum_range_measure_preimage_singleton`, `SimpleFunc.approxOn_range_nonneg` bridge: `SimpleFunc.hasBoxIntegral`, `SimpleFunc.box_integral_eq_integral`

MeasureTheory.SimpleFunc

Definitions

Name	Category	Theorems
`FinMeasSupp` 📖	MathDef	7 math math: `FinMeasSupp.of_lintegral_ne_top`, `FinMeasSupp.map_iff`, `memLp_iff_finMeasSupp`, `FinMeasSupp.iff_lintegral_lt_top`, `integrable_iff_finMeasSupp`, `finMeasSupp_iff`, `finMeasSupp_iff_support`
`approx` 📖	CompOp	4 math math: `iSup_approx_apply`, `approx_comp`, `approx_apply`, `monotone_approx`
`bind` 📖	CompOp	2 math math: `bind_apply`, `bind_const`
`comp` 📖	CompOp	5 math math: `range_comp_subset_range`, `approxOn_comp`, `coe_comp`, `extend_comp_eq`, `lintegral_map`
`const` 📖	CompOp	26 math math: `range_indicator`, `MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst`, `const_apply`, `setToSimpleFunc_const`, `const_add_eq_map`, `const_lintegral_restrict`, `restrict_const_lintegral`, `map_const`, `const_one`, `support_indicator`, `const_mul_eq_map`, `const_lintegral`, `simpleFunc_bot'`, `setToSimpleFunc_indicator`, `const_algebraMap`, `nearestPt_zero`, `range_const`, `smul_const`, `const_mul_lintegral`, `integral_const`, `range_const_subset`, `setToSimpleFunc_const'`, `const_zero`, `bind_const`, `coe_const`, `nearestPtInd_zero`
`eapprox` 📖	CompOp	10 math math: `MeasureTheory.measure_support_eapprox_lt_top`, `iSup_coe_eapprox`, `tendsto_eapprox`, `MeasureTheory.lintegral_eapprox_le_lintegral`, `eapprox_comp`, `sum_eapproxDiff`, `monotone_eapprox`, `iSup_eapprox_apply`, `eapprox_lt_top`, `MeasureTheory.lintegral_eq_iSup_eapprox_lintegral`
`eapproxDiff` 📖	CompOp	2 math math: `sum_eapproxDiff`, `tsum_eapproxDiff`
`ennrealRatEmbed` 📖	CompOp	1 math math: `ennrealRatEmbed_encode`
`extend` 📖	CompOp	4 math math: `extend_apply'`, `extend_comp_eq`, `extend_comp_eq'`, `extend_apply`
`hasIntPow` 📖	CompOp	2 math math: `coe_zpow`, `zpow_apply`
`hasNatPow` 📖	CompOp	2 math math: `coe_pow`, `pow_apply`
`hasNatSMul` 📖	CompOp	—
`instAdd` 📖	CompOp	10 math math: `const_add_eq_map`, `coe_add`, `map_add`, `setToSimpleFunc_add`, `add_lintegral`, `FinMeasSupp.add`, `integral_add`, `add_eq_map₂`, `add_apply`, `MeasureTheory.Lp.simpleFunc.toLp_add`
`instAddCommGroup` 📖	CompOp	—
`instAddCommMonoid` 📖	CompOp	1 math math: `instIsOrderedAddMonoid`
`instAddGroup` 📖	CompOp	—
`instAddMonoid` 📖	CompOp	—
`instAlgebra` 📖	CompOp	2 math math: `const_algebraMap`, `coe_algebraMap`
`instBoundedOrder` 📖	CompOp	—
`instCommGroup` 📖	CompOp	—
`instCommMonoid` 📖	CompOp	1 math math: `instIsOrderedMonoid`
`instCommRing` 📖	CompOp	—
`instCommSemiring` 📖	CompOp	—
`instDiv` 📖	CompOp	2 math math: `div_apply`, `coe_div`
`instFunLike` 📖	CompOp	185 math, 2 bridge math: `coe_range`, `exists_forall_le`, `MeasureTheory.lintegral_def`, `sum_measure_preimage_singleton`, `coe_zpow`, `coe_lt_coe`, `MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst`, `MeasureTheory.MemLp.exists_simpleFunc_eLpNorm_sub_lt`, `MeasureTheory.StronglyMeasurable.tendsto_approxBounded_ae`, `forall_mem_range`, `Measurable.add_simpleFunc`, `coe_sup`, `MeasureTheory.Integrable.simpleFunc_mul'`, `tendsto_approxOn_range_L1_enorm`, `MeasureTheory.measure_support_eapprox_lt_top`, `nearestPtInd_succ`, `const_apply`, `measurable_bind`, `memLp_zero`, `apply_mk`, `MeasureTheory.FinStronglyMeasurable.tendsto_approx`, `MeasureTheory.Integrable.simpleFunc_mul`, `piecewise_apply`, `iSup_coe_eapprox`, `restrict_lintegral`, `integral_eq_sum_filter`, `mem_range`, `coe_add`, `memLp_iff_integrable`, `MeasureTheory.Lp.simpleFunc.stronglyMeasurable`, `MeasureTheory.Lp.simpleFunc.sub_toSimpleFunc`, `tendsto_eapprox`, `finite_range`, `MeasureTheory.Lp.simpleFunc.smul_toSimpleFunc`, `coe_piecewise`, `coe_star`, `coe_le`, `nnnorm_approxOn_le`, `exists_forall_norm_le`, `pair_preimage_singleton`, `preimage_eq_empty_iff`, `measurable`, `coe_zero`, `memLp_iff_finMeasSupp`, `MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos`, `lintegral_restrict`, `MeasureTheory.condExp_stronglyMeasurable_simpleFunc_mul`, `MeasureTheory.Lp.simpleFunc.add_toSimpleFunc`, `norm_approxOn_y₀_le`, `eapprox_comp`, `nearestPtInd_le`, `map_lintegral`, `coe_mul`, `memLp_approxOn_range`, `memLp_iff`, `MeasureTheory.tendsto_setToFun_approxOn_of_measurable_of_range_subset`, `edist_approxOn_y0_le`, `norm_setToSimpleFunc_le_sum_mul_norm`, `coe_map`, `edist_approxOn_mono`, `MeasureTheory.condExp_stronglyMeasurable_simpleFunc_bilin`, `approxOn_mem`, `sum_eapproxDiff`, `support_indicator`, `coe_pow`, `coe_natCast`, `MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul`, `exists_range_iff`, `lintegral_eq_of_subset'`, `norm_setToSimpleFunc_le_sum_opNorm`, `FinMeasSupp.integrable`, `pair_preimage`, `MeasureTheory.exists_lt_lintegral_simpleFunc_of_lt_lintegral`, `coe_toLargerSpace_eq`, `vadd_apply`, `FinMeasSupp.meas_preimage_singleton_ne_zero`, `memLp_top`, `coe_vadd`, `integrable_iff`, `neg_apply`, `tendsto_approxOn`, `inv_apply`, `MeasureTheory.Lp.simpleFunc.neg_toSimpleFunc`, `ext_iff`, `MeasureTheory.L1.SimpleFunc.integrable`, `coe_le_coe`, `MeasureTheory.Lp.simpleFunc.memLp`, `MeasureTheory.Lp.simpleFunc.norm_toSimpleFunc`, `MeasureTheory.L1.SimpleFunc.negPart_toSimpleFunc`, `measurableSet_support`, `memLp_approxOn`, `Measurable.simpleFunc_add`, `coe_smul`, `bind_apply`, `MeasureTheory.L1.SimpleFunc.posPart_toSimpleFunc`, `sup_apply`, `measure_support_lt_top_of_lintegral_ne_top`, `coe_mk`, `coe_neg`, `integrable_approxOn_range`, `exists_le_lowerSemicontinuous_lintegral_ge`, `div_apply`, `coe_sub`, `coe_restrict`, `integral_eq_sum_of_subset`, `seq_apply`, `mem_restrict_range`, `eLpNorm'_eq`, `measurableSet_preimage`, `MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq`, `tendsto_nearestPt`, `memLp_of_isFiniteMeasure`, `coe_comp`, `sub_apply`, `integrable_approxOn`, `pair_apply`, `MeasureTheory.StronglyMeasurable.tendsto_approx`, `integrable_of_isFiniteMeasure`, `coe_div`, `measurableSet_fiber`, `pow_apply`, `restrict_apply`, `stronglyMeasurable`, `coe_inf`, `setToSimpleFunc_eq_sum_filter`, `simpleFunc_bot`, `norm_approxOn_zero_le`, `aemeasurable`, `iSup_eapprox_apply`, `zpow_apply`, `MeasureTheory.Lp.simpleFunc.aestronglyMeasurable`, `ProbabilityTheory.strong_law_ae_simpleFunc_comp`, `mem_image_of_mem_range_restrict`, `exists_upperSemicontinuous_le_lintegral_le`, `aestronglyMeasurable`, `measurableSet_cut`, `coe_intCast`, `MeasureTheory.Lp.simpleFunc.measurable`, `MeasureTheory.StronglyMeasurable.stronglyMeasurable_in_set`, `integrable_iff_finMeasSupp`, `HasCompactSupport.exists_simpleFunc_approx_of_prod`, `integral_eq`, `MeasureTheory.tendsto_setToFun_approxOn_of_measurable`, `extend_apply'`, `tsum_eapproxDiff`, `iSup_approx_apply`, `MeasureTheory.FinStronglyMeasurable.fin_support_approx`, `map_apply`, `eapprox_lt_top`, `inf_apply`, `mem_range_self`, `support_eq`, `tendsto_approxOn_L1_enorm`, `approx_comp`, `edist_nearestPt_le`, `restrict_preimage`, `approx_apply`, `coe_one`, `finMeasSupp_iff`, `finset_sup_apply`, `map_preimage`, `MeasureTheory.tendsto_integral_norm_approxOn_sub`, `edist_approxOn_le`, `MeasureTheory.Lp.simpleFunc.toSimpleFunc_eq_toFun`, `coe_algebraMap`, `coe_const`, `coe_inv`, `smul_apply`, `tendsto_approxOn_range_Lp`, `extend_comp_eq'`, `add_apply`, `MeasureTheory.StronglyMeasurable.norm_approxBounded_le`, `MeasureTheory.Lp.simpleFunc.aemeasurable`, `mul_apply`, `tendsto_approxOn_Lp_eLpNorm`, `approxOn_zero`, `MeasureTheory.StronglyMeasurable.tendsto_approxBounded_of_norm_le`, `extend_apply`, `restrict_preimage_singleton`, `finMeasSupp_iff_support`, `lintegral_eq_lintegral`, `MeasureTheory.Lp.simpleFunc.zero_toSimpleFunc`, `tendsto_approxOn_range_Lp_eLpNorm`, `map_preimage_singleton`, `sum_range_measure_preimage_singleton` bridge: `hasBoxIntegral`, `box_integral_eq_integral`
`instGroup` 📖	CompOp	—
`instInf` 📖	CompOp	2 math math: `coe_inf`, `inf_apply`
`instInhabited` 📖	CompOp	—
`instIntCast` 📖	CompOp	1 math math: `coe_intCast`
`instInv` 📖	CompOp	2 math math: `inv_apply`, `coe_inv`
`instInvolutiveStar` 📖	CompOp	—
`instLE` 📖	CompOp	6 math math: `coe_le`, `piecewise_mono`, `mk_le_mk`, `coe_le_coe`, `MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq`, `approxOn_range_nonneg`
`instLattice` 📖	CompOp	—
`instModule` 📖	CompOp	—
`instMonoid` 📖	CompOp	—
`instMul` 📖	CompOp	7 math math: `map_mul`, `mul_eq_map₂`, `coe_mul`, `FinMeasSupp.mul`, `const_mul_eq_map`, `const_mul_lintegral`, `mul_apply`
`instMulAction` 📖	CompOp	—
`instNatCast` 📖	CompOp	1 math math: `coe_natCast`
`instNeg` 📖	CompOp	5 math math: `integral_neg`, `setToSimpleFunc_neg`, `neg_apply`, `coe_neg`, `MeasureTheory.Lp.simpleFunc.toLp_neg`
`instNonAssocRing` 📖	CompOp	—
`instNonAssocSemiring` 📖	CompOp	—
`instNonUnitalCommRing` 📖	CompOp	—
`instNonUnitalCommSemiring` 📖	CompOp	—
`instNonUnitalNonAssocSemiring` 📖	CompOp	—
`instNonUnitalRing` 📖	CompOp	—
`instNonUnitalSemiring` 📖	CompOp	—
`instOne` 📖	CompOp	3 math math: `const_one`, `range_one`, `coe_one`
`instOrderBot` 📖	CompOp	1 math math: `finset_sup_apply`
`instOrderTop` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	2 math math: `instIsOrderedAddMonoid`, `instIsOrderedMonoid`
`instPreorder` 📖	CompOp	4 math math: `coe_lt_coe`, `monotone_eapprox`, `mk_lt_mk`, `monotone_approx`
`instRing` 📖	CompOp	—
`instSMul` 📖	CompOp	10 math math: `setToSimpleFunc_smul`, `coe_smul`, `smul_eq_map`, `smul_const`, `MeasureTheory.Lp.simpleFunc.toLp_smul`, `integral_smul`, `instIsScalarTower`, `setToSimpleFunc_smul_real`, `smul_apply`, `instSMulCommClass`
`instSemilatticeInf` 📖	CompOp	—
`instSemilatticeSup` 📖	CompOp	1 math math: `finset_sup_apply`
`instSemiring` 📖	CompOp	2 math math: `const_algebraMap`, `coe_algebraMap`
`instStar` 📖	CompOp	1 math math: `coe_star`
`instStarAddMonoid` 📖	CompOp	—
`instStarMul` 📖	CompOp	—
`instStarRing` 📖	CompOp	—
`instSub` 📖	CompOp	7 math math: `posPart_sub_negPart`, `MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos`, `setToSimpleFunc_sub`, `integral_sub`, `coe_sub`, `MeasureTheory.Lp.simpleFunc.toLp_sub`, `sub_apply`
`instSup` 📖	CompOp	4 math math: `coe_sup`, `le_sup_lintegral`, `sup_apply`, `sup_eq_map₂`
`instVAdd` 📖	CompOp	2 math math: `vadd_apply`, `coe_vadd`
`instZero` 📖	CompOp	11 math math: `integral_piecewise_zero`, `setToSimpleFunc_zero_apply`, `coe_zero`, `range_zero`, `restrict_empty`, `MeasureTheory.Lp.simpleFunc.toLp_zero`, `restrict_of_not_measurable`, `MeasureTheory.Lp.simpleFunc.exists_simpleFunc_nonneg_ae_eq`, `const_zero`, `zero_lintegral`, `approxOn_range_nonneg`
`lintegral` 📖	CompOp	34 math math: `MeasureTheory.lintegral_def`, `lintegral_mono_fun`, `lintegral_sum`, `restrict_lintegral`, `lintegral_congr`, `const_lintegral_restrict`, `restrict_const_lintegral`, `MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos`, `lintegral_restrict`, `MeasureTheory.lintegral_eapprox_le_lintegral`, `le_sup_lintegral`, `map_lintegral`, `FinMeasSupp.iff_lintegral_lt_top`, `lintegral_eq_of_subset'`, `lintegral_zero`, `add_lintegral`, `lintegral_eq_of_measure_preimage`, `lintegral_smul`, `const_lintegral`, `FinMeasSupp.lintegral_lt_top`, `MeasureTheory.lintegral_eq_nnreal`, `lintegral_restrict_iUnion_of_directed`, `lintegral_map'`, `lintegral_mono`, `restrict_lintegral_eq_lintegral_restrict`, `lintegral_add`, `lintegral_eq_of_subset`, `const_mul_lintegral`, `lintegral_finset_sum`, `lintegral_map`, `MeasureTheory.lintegral_eq_iSup_eapprox_lintegral`, `lintegral_mono_measure`, `lintegral_eq_lintegral`, `zero_lintegral`
`lintegralₗ` 📖	CompOp	—
`map` 📖	CompOp	34 math math: `posPart_map_norm`, `map_mul`, `const_add_eq_map`, `FinMeasSupp.map_iff`, `map_fst_pair`, `mul_eq_map₂`, `map_add`, `MeasureTheory.exists_simpleFunc_forall_lintegral_sub_lt_of_pos`, `map_restrict_of_zero`, `map_const`, `map_lintegral`, `coe_map`, `negPart_map_norm`, `const_mul_eq_map`, `map_snd_pair`, `norm_integral_le_integral_norm`, `MeasureTheory.lintegral_eq_nnreal`, `map_coe_nnreal_restrict`, `map_map`, `smul_eq_map`, `MeasureTheory.L1.SimpleFunc.norm_eq_integral`, `FinMeasSupp.map₂`, `map_integral`, `map_apply`, `norm_setToSimpleFunc_le_integral_norm`, `FinMeasSupp.map`, `map_preimage`, `sup_eq_map₂`, `add_eq_map₂`, `integral_eq_lintegral'`, `range_map`, `map_coe_ennreal_restrict`, `map_setToSimpleFunc`, `map_preimage_singleton`
`ofFinite` 📖	CompOp	—
`ofIsEmpty` 📖	CompOp	—
`pair` 📖	CompOp	11 math math: `map_fst_pair`, `mul_eq_map₂`, `pair_preimage_singleton`, `pair_preimage`, `map_snd_pair`, `integrable_pair`, `pair_apply`, `FinMeasSupp.map₂`, `FinMeasSupp.pair`, `sup_eq_map₂`, `add_eq_map₂`
`piecewise` 📖	CompOp	12 math math: `range_indicator`, `integral_piecewise_zero`, `MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst`, `piecewise_compl`, `piecewise_apply`, `coe_piecewise`, `piecewise_mono`, `support_indicator`, `setToSimpleFunc_indicator`, `piecewise_empty`, `piecewise_same`, `piecewise_univ`
`range` 📖	CompOp	34 math math: `coe_range`, `range_indicator`, `range_comp_subset_range`, `restrict_lintegral`, `integral_eq_sum_filter`, `mem_range`, `mem_range_of_measure_ne_zero`, `preimage_eq_empty_iff`, `lintegral_restrict`, `integral_eq_sum`, `map_lintegral`, `norm_setToSimpleFunc_le_sum_mul_norm`, `range_zero`, `MeasureTheory.L1.SimpleFunc.norm_eq_sum_mul`, `exists_range_iff`, `norm_setToSimpleFunc_le_sum_opNorm`, `MeasureTheory.integral_simpleFunc_larger_space`, `mem_restrict_range`, `eLpNorm'_eq`, `range_eq_empty_of_isEmpty`, `range_one`, `range_const`, `setToSimpleFunc_eq_sum_filter`, `norm_setToSimpleFunc_le_sum_mul_norm_of_integrable`, `range_const_subset`, `integral_eq`, `map_integral`, `mem_range_self`, `support_eq`, `map_preimage`, `range_map`, `map_setToSimpleFunc`, `map_preimage_singleton`, `sum_range_measure_preimage_singleton`
`restrict` 📖	CompOp	15 math math: `restrict_univ`, `restrict_lintegral`, `restrict_const_lintegral`, `map_restrict_of_zero`, `restrict_mono`, `restrict_empty`, `coe_restrict`, `restrict_of_not_measurable`, `map_coe_nnreal_restrict`, `mem_restrict_range`, `restrict_lintegral_eq_lintegral_restrict`, `restrict_apply`, `restrict_preimage`, `restrict_preimage_singleton`, `map_coe_ennreal_restrict`
`seq` 📖	CompOp	1 math math: `seq_apply`
`toFun` 📖	CompOp	2 math math: `finite_range'`, `measurableSet_fiber'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instAdd`	—	—
`add_eq_map₂` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instAdd` `map` `pair`	—	—
`add_lintegral` 📖	mathematical	—	`lintegral` `MeasureTheory.SimpleFunc` `ENNReal` `instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`add_eq_map₂` `map_lintegral` `Finset.sum_congr` `add_mul` `Distrib.rightDistribClass` `Finset.sum_add_distrib`
`aemeasurable` 📖	mathematical	—	`AEMeasurable` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Measurable.aemeasurable` `measurable`
`apply_mk` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set` `Set.instSingletonSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	—
`approx_apply` 📖	mathematical	`Measurable`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `approx` `Finset.sup` `Finset.range` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`finset_sup_apply` `restrict_apply` `measurableSet_Ici` `instClosedIciTopology` `Set.indicator_apply`
`approx_comp` 📖	mathematical	`Measurable`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `approx`	—	`approx_apply` `Measurable.comp`
`bind_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `bind`	—	—
`bind_const` 📖	mathematical	—	`bind` `const`	—	`ext`
`coe_add` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_algebraMap` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instSemiring` `RingHom.instFunLike` `algebraMap` `instAlgebra` `Pi.semiring` `Function.algebra`	—	—
`coe_comp` 📖	mathematical	`Measurable`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `comp`	—	—
`coe_const` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `const`	—	—
`coe_div` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instDiv` `Pi.instDiv`	—	—
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instInf` `Pi.instMinForall_mathlib`	—	—
`coe_injective` 📖	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	—	`DFunLike.ext'`
`coe_intCast` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instIntCast`	—	—
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instInv` `Pi.instInv`	—	—
`coe_le` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instLE`	—	`coe_le_coe`
`coe_le_coe` 📖	mathematical	—	`Pi.hasLe` `Preorder.toLE` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instLE`	—	—
`coe_lt_coe` 📖	mathematical	—	`Preorder.toLT` `Pi.preorder` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instPreorder`	—	—
`coe_map` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `map`	—	—
`coe_mk` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set` `Set.instSingletonSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_natCast` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instNatCast`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instNeg` `Pi.instNeg`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instOne` `Pi.instOne`	—	—
`coe_piecewise` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `piecewise` `Set.piecewise` `Set` `Set.instMembership`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `hasNatPow` `Pi.instPow` `Monoid.toNatPow`	—	—
`coe_range` 📖	mathematical	—	`SetLike.coe` `Finset` `Finset.instSetLike` `range` `Set.range` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Set.Finite.coe_toFinset` `finite_range`
`coe_restrict` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `restrict` `Set.indicator`	—	`restrict.eq_1` `coe_piecewise` `coe_zero` `Set.piecewise_eq_indicator`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSMul` `Function.hasSMul`	—	—
`coe_star` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `Star.star` `instStar` `Pi.instStarForall`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSub` `Pi.instSub`	—	—
`coe_sup` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSup` `Pi.instMaxForall_mathlib`	—	—
`coe_vadd` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Function.hasVAdd`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instZero` `Pi.instZero`	—	—
`coe_zpow` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `hasIntPow` `Pi.instPow` `DivInvMonoid.toZPow`	—	—
`const_add_eq_map` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instAdd` `const` `map`	—	—
`const_algebraMap` 📖	mathematical	—	`const` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `MeasureTheory.SimpleFunc` `instSemiring` `instAlgebra`	—	—
`const_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `const`	—	—
`const_lintegral` 📖	mathematical	—	`lintegral` `const` `ENNReal` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.univ`	—	`lintegral.eq_1` `isEmpty_or_nonempty` `Finset.sum_congr` `range_eq_empty_of_isEmpty` `MeasureTheory.Measure.eq_zero_of_isEmpty` `MulZeroClass.mul_zero` `Finset.sum_const_zero` `range_const` `Finset.sum_singleton` `Set.preimage_const_of_mem` `Set.mem_singleton`
`const_lintegral_restrict` 📖	mathematical	—	`lintegral` `const` `ENNReal` `MeasureTheory.Measure.restrict` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`const_lintegral` `MeasureTheory.Measure.restrict_apply` `MeasurableSet.univ` `Set.univ_inter`
`const_mul_eq_map` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instMul` `const` `map`	—	—
`const_mul_lintegral` 📖	mathematical	—	`lintegral` `MeasureTheory.SimpleFunc` `ENNReal` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `const`	—	`map_lintegral` `Finset.mul_sum` `Finset.sum_congr` `mul_assoc`
`const_one` 📖	mathematical	—	`const` `MeasureTheory.SimpleFunc` `instOne`	—	—
`const_zero` 📖	mathematical	—	`const` `MeasureTheory.SimpleFunc` `instZero`	—	—
`div_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instDiv`	—	—
`eapprox_comp` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `eapprox`	—	`approx_comp` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `BorelSpace.opensMeasurable` `ENNReal.borelSpace`
`eapprox_lt_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `eapprox` `Top.top` `instTopENNReal`	—	`finset_sup_apply` `Finset.sup_lt_iff` `WithTop.top_pos` `Set.piecewise_eq_indicator` `Set.indicator_le_self` `ENNReal.instCanonicallyOrderedAdd` `ENNReal.coe_lt_top`
`ennrealRatEmbed_encode` 📖	mathematical	—	`ennrealRatEmbed` `Encodable.encode` `Rat.instEncodable` `ENNReal.ofNNReal` `Real.toNNReal` `Real` `Real.instRatCast`	—	`ennrealRatEmbed.eq_1` `Encodable.encodek`
`eq_zero_of_mem_range_zero` 📖	—	`Finset` `Finset.instMembership` `range` `MeasureTheory.SimpleFunc` `instZero`	—	—	`forall_mem_range`
`exists_forall_le` 📖	mathematical	—	`Preorder.toLE` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`forall_mem_range` `Finset.exists_le`
`exists_range_iff` 📖	mathematical	—	`Finset` `Finset.instMembership` `range` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Set.exists_range_iff`
`ext` 📖	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`ext`
`extend_apply` 📖	mathematical	`MeasurableEmbedding`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `extend`	—	`Function.Injective.extend_apply` `MeasurableEmbedding.injective`
`extend_apply'` 📖	mathematical	`MeasurableEmbedding`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `extend`	—	`Function.extend_apply'`
`extend_comp_eq` 📖	mathematical	`MeasurableEmbedding`	`comp` `extend` `MeasurableEmbedding.measurable`	—	`coe_injective` `MeasurableEmbedding.measurable` `extend_comp_eq'`
`extend_comp_eq'` 📖	mathematical	`MeasurableEmbedding`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `extend`	—	`extend_apply`
`finMeasSupp_iff` 📖	mathematical	—	`FinMeasSupp` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet` `Top.top` `instTopENNReal`	—	`lt_of_le_of_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `finMeasSupp_iff_support` `support_eq` `MeasureTheory.measure_biUnion_lt_top` `Finset.finite_toSet` `Finset.mem_filter`
`finMeasSupp_iff_support` 📖	mathematical	—	`FinMeasSupp` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Function.support` `MeasureTheory.SimpleFunc` `instFunLike` `Top.top` `instTopENNReal`	—	—
`finite_range` 📖	mathematical	—	`Set.Finite` `Set.range` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`finite_range'`
`finite_range'` 📖	mathematical	—	`Set.Finite` `Set.range` `toFun`	—	—
`finset_sup_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `Finset.sup` `instSemilatticeSup` `instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`Finset.induction_on` `Finset.sup_insert` `sup_apply`
`forall_mem_range` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	—
`iSup_approx_apply` 📖	mathematical	`Measurable` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `approx` `ConditionallyCompleteLattice.toLattice` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder`	—	`le_antisymm` `iSup_le` `approx_apply` `Finset.sup_le` `le_iSup_of_le` `le_iSup` `bot_le` `Finset.mem_range` `le_trans` `le_of_eq` `Finset.le_sup`
`iSup_coe_eapprox` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`iSup` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `eapprox`	—	`iSup_apply` `iSup_eapprox_apply`
`iSup_eapprox_apply` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `eapprox`	—	`eapprox.eq_1` `iSup_approx_apply` `OrderTopology.to_orderClosedTopology` `ENNReal.instOrderTopology` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `le_antisymm` `iSup_le` `le_of_not_gt` `ENNReal.lt_iff_exists_rat_btwn` `le_iSup_of_le` `ennrealRatEmbed_encode` `le_of_lt` `le_rfl` `lt_irrefl` `lt_of_le_of_lt`
`induction` 📖	—	`piecewise` `const` `AddZero.toZero` `AddZeroClass.toAddZero` `MeasureTheory.SimpleFunc` `instAdd` `AddZero.toAdd`	—	—	`Finset.induction` `MeasurableSet.univ` `ext` `Set.range_subset_singleton` `Set.diff_eq_empty` `Finset.coe_empty` `piecewise_same` `measurableSet_preimage` `Set.range_piecewise` `Set.image_compl_preimage` `Set.union_diff_distrib` `Set.diff_diff_comm` `Finset.coe_insert` `Set.insert_diff_self_of_notMem` `Finset.mem_coe` `Set.image_subset_iff` `Set.preimage_const_of_mem` `Set.mem_singleton` `Set.subset_univ` `Set.empty_union` `Set.piecewise_eq_indicator` `Set.piecewise_eq_of_mem` `Set.indicator_of_mem` `zero_add` `Set.piecewise_eq_of_notMem` `Set.indicator_of_notMem` `add_zero` `disjoint_iff_inf_le` `Set.support_indicator` `coe_range` `Finset.coe_singleton` `Finset.coe_sdiff`
`induction'` 📖	—	`const` `piecewise`	—	—	`Finset.induction` `ext` `Set.range_subset_singleton` `Set.diff_eq_empty` `Finset.coe_empty` `measurableSet_preimage` `Set.range_piecewise` `Set.image_compl_preimage` `Set.union_diff_distrib` `Set.diff_diff_comm` `Finset.coe_insert` `Set.insert_diff_self_of_notMem` `Finset.mem_coe` `Set.image_subset_iff` `Set.preimage_const_of_mem` `Set.mem_singleton` `Set.subset_univ` `Set.empty_union` `MeasurableSet.compl` `MeasurableSet.of_compl` `piecewise_compl` `Set.piecewise_eq_of_mem` `Set.piecewise_eq_of_notMem` `coe_range` `Finset.coe_singleton` `Finset.coe_sdiff`
`inf_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instInf`	—	—
`instIsOrderedAddMonoid` 📖	mathematical	—	`IsOrderedAddMonoid` `MeasureTheory.SimpleFunc` `instAddCommMonoid` `instPartialOrder`	—	`add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono`
`instIsOrderedMonoid` 📖	mathematical	—	`IsOrderedMonoid` `MeasureTheory.SimpleFunc` `instCommMonoid` `instPartialOrder`	—	`mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `MeasureTheory.SimpleFunc` `instSMul`	—	`ext` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `MeasureTheory.SimpleFunc` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instInv`	—	—
`le_sup_lintegral` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.instMax` `lintegral` `MeasureTheory.SimpleFunc` `instSup`	—	`Monotone.le_map_sup` `lintegral_mono_fun`
`lintegral_add` 📖	mathematical	—	`lintegral` `MeasureTheory.Measure` `MeasureTheory.Measure.instAdd` `ENNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`LinearMap.map_add` `IsScalarTower.right` `Algebra.to_smulCommClass`
`lintegral_congr` 📖	mathematical	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	`lintegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `lintegral_eq_of_measure_preimage` `MeasureTheory.measure_congr` `Filter.Eventually.set_eq` `Filter.Eventually.mono`
`lintegral_eq_of_measure_preimage` 📖	mathematical	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet`	`lintegral`	—	`Finset.sum_congr` `lintegral_eq_of_subset` `mem_range_of_measure_ne_zero`
`lintegral_eq_of_subset` 📖	mathematical	`ENNReal` `Finset` `Finset.instMembership` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	`lintegral` `Finset.sum` `ENNReal.instAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `Set.instSingletonSet`	—	`Finset.sum_bij_ne_zero` `ENNReal.instNoZeroDivisors` `mem_range` `Set.preimage_singleton_nonempty` `MeasureTheory.nonempty_of_measure_ne_zero` `mul_ne_zero_iff`
`lintegral_eq_of_subset'` 📖	mathematical	`Finset` `ENNReal` `Finset.instHasSubset` `Finset.instSDiff` `LinearOrder.toDecidableEq` `ENNReal.instLinearOrder` `range` `Finset.instSingleton` `instZeroENNReal`	`lintegral` `Finset.sum` `ENNReal.instAddCommMonoid` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet`	—	`lintegral_eq_of_subset` `Finset.mem_sdiff` `mem_range_self` `Finset.mem_singleton`
`lintegral_finset_sum` 📖	mathematical	—	`lintegral` `Finset.sum` `MeasureTheory.Measure` `MeasureTheory.Measure.instAddCommMonoid` `ENNReal` `ENNReal.instAddCommMonoid`	—	`map_sum` `IsScalarTower.right` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `Algebra.to_smulCommClass`
`lintegral_map` 📖	mathematical	`Measurable`	`lintegral` `MeasureTheory.Measure.map` `comp` `ENNReal`	—	`lintegral_map'` `MeasureTheory.Measure.map_apply`
`lintegral_map'` 📖	mathematical	`DFunLike.coe` `MeasureTheory.SimpleFunc` `ENNReal` `instFunLike` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage`	`lintegral`	—	`lintegral_eq_of_measure_preimage` `measurableSet_preimage`
`lintegral_mono` 📖	mathematical	`MeasureTheory.SimpleFunc` `ENNReal` `instLE` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.Measure` `MeasureTheory.Measure.instPartialOrder`	`lintegral`	—	`LE.le.trans` `lintegral_mono_fun` `lintegral_mono_measure`
`lintegral_mono_fun` 📖	mathematical	`MeasureTheory.SimpleFunc` `ENNReal` `instLE` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder`	`lintegral`	—	`Monotone.of_left_le_map_sup` `map_fst_pair` `map_lintegral` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `le_sup_left`
`lintegral_mono_measure` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `MeasureTheory.Measure.instPartialOrder`	`ENNReal` `ENNReal.instPartialOrder` `lintegral`	—	`Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `MeasureTheory.Measure.measure_mono_left`
`lintegral_restrict` 📖	mathematical	—	`lintegral` `MeasureTheory.Measure.restrict` `Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet`	—	`Finset.sum_congr` `MeasureTheory.Measure.restrict_apply` `measurableSet_preimage`
`lintegral_restrict_iUnion_of_directed` 📖	mathematical	`Directed` `Set` `Set.instHasSubset`	`lintegral` `MeasureTheory.Measure.restrict` `Set.iUnion` `iSup` `ENNReal` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `ENNReal.instCompleteLinearOrder`	—	`Finset.sum_congr` `MeasureTheory.Measure.restrict_iUnion_apply_eq_iSup` `measurableSet_preimage` `ENNReal.mul_iSup` `ENNReal.finsetSum_iSup` `mul_le_mul_right` `IsOrderedMonoid.toMulLeftMono` `ENNReal.instIsOrderedMonoid` `MeasureTheory.Measure.measure_mono_left` `MeasureTheory.Measure.restrict_mono` `le_refl`
`lintegral_smul` 📖	mathematical	—	`lintegral` `MeasureTheory.Measure` `MeasureTheory.Measure.instSMul` `ENNReal`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `smul_one_smul` `MeasureTheory.Measure.instIsScalarTower` `LinearMap.map_smul`
`lintegral_sum` 📖	mathematical	—	`lintegral` `MeasureTheory.Measure.sum` `tsum` `ENNReal` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `SummationFilter.unconditional`	—	`Finset.sum_congr` `MeasureTheory.Measure.sum_apply` `measurableSet_preimage` `ENNReal.tsum_comm`
`lintegral_zero` 📖	mathematical	—	`lintegral` `MeasureTheory.Measure` `MeasureTheory.Measure.instZero` `ENNReal` `instZeroENNReal`	—	`LinearMap.map_zero` `IsScalarTower.right` `Algebra.to_smulCommClass`
`map_add` 📖	mathematical	—	`map` `MeasureTheory.SimpleFunc` `instAdd`	—	`ext`
`map_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `map`	—	—
`map_coe_ennreal_restrict` 📖	mathematical	—	`map` `NNReal` `ENNReal` `ENNReal.ofNNReal` `restrict` `instZeroNNReal` `instZeroENNReal`	—	`map_restrict_of_zero` `ENNReal.coe_zero`
`map_coe_nnreal_restrict` 📖	mathematical	—	`map` `NNReal` `Real` `NNReal.toReal` `restrict` `instZeroNNReal` `Real.instZero`	—	`map_restrict_of_zero` `NNReal.coe_zero`
`map_const` 📖	mathematical	—	`map` `const`	—	—
`map_fst_pair` 📖	mathematical	—	`map` `pair`	—	—
`map_lintegral` 📖	mathematical	—	`lintegral` `map` `ENNReal` `Finset.sum` `ENNReal.instAddCommMonoid` `range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet`	—	`Finset.sum_congr` `range_map` `Finset.sum_image'` `mem_range` `map_preimage_singleton` `sum_measure_preimage_singleton` `Finset.mul_sum`
`map_map` 📖	mathematical	—	`map`	—	—
`map_mul` 📖	mathematical	—	`map` `MeasureTheory.SimpleFunc` `instMul`	—	`ext`
`map_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `map` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.filter` `Set` `Set.instMembership` `range`	—	`Finset.filter.congr_simp` `Finset.coe_filter` `coe_range` `Set.inter_comm` `Set.preimage_inter_range` `Set.preimage_comp`
`map_preimage_singleton` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `map` `Set` `Set.instSingletonSet` `SetLike.coe` `Finset` `Finset.instSetLike` `Finset.filter` `range`	—	`map_preimage`
`map_restrict_of_zero` 📖	mathematical	—	`map` `restrict`	—	`ext` `coe_restrict` `Set.indicator_comp_of_zero` `restrict_of_not_measurable`
`map_snd_pair` 📖	mathematical	—	`map` `pair`	—	—
`measurable` 📖	mathematical	—	`Measurable` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`measurableSet_preimage`
`measurableSet_cut` 📖	mathematical	`MeasurableSet` `setOf`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Set.ext` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_iUnion_eq'` `MeasurableSet.biUnion` `Set.Finite.countable` `finite_range` `MeasurableSet.inter` `measurableSet_fiber`
`measurableSet_fiber` 📖	mathematical	—	`MeasurableSet` `Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `Set` `Set.instSingletonSet`	—	`measurableSet_fiber'`
`measurableSet_fiber'` 📖	mathematical	—	`MeasurableSet` `Set.preimage` `toFun` `Set` `Set.instSingletonSet`	—	—
`measurableSet_preimage` 📖	mathematical	—	`MeasurableSet` `Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`measurableSet_cut` `MeasurableSet.const`
`measurableSet_support` 📖	mathematical	—	`MeasurableSet` `Function.support` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`support_eq` `Finset.measurableSet_biUnion` `measurableSet_fiber`
`measurable_bind` 📖	mathematical	`Measurable`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`measurableSet_cut`
`measure_support_lt_top` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet` `Top.top` `instTopENNReal`	`Function.support`	—	`support_eq` `LE.le.trans_lt` `MeasureTheory.measure_biUnion_finset_le` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.sum_lt_top` `Finset.mem_filter`
`measure_support_lt_top_of_lintegral_ne_top` 📖	mathematical	—	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Function.support` `instZeroENNReal` `MeasureTheory.SimpleFunc` `instFunLike` `Top.top` `instTopENNReal`	—	`measure_support_lt_top` `finMeasSupp_iff` `FinMeasSupp.of_lintegral_ne_top`
`mem_image_of_mem_range_restrict` 📖	mathematical	`Finset` `Finset.instMembership` `range` `restrict`	`Set` `Set.instMembership` `Set.image` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`mem_restrict_range` `eq_zero_of_mem_range_zero` `restrict_of_not_measurable`
`mem_range` 📖	mathematical	—	`Finset` `Finset.instMembership` `range` `Set` `Set.instMembership` `Set.range` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Set.Finite.mem_toFinset` `finite_range`
`mem_range_of_measure_ne_zero` 📖	mathematical	—	`Finset` `Finset.instMembership` `range`	—	`MeasureTheory.nonempty_of_measure_ne_zero` `mem_range`
`mem_range_self` 📖	mathematical	—	`Finset` `Finset.instMembership` `range` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`mem_range`
`mem_restrict_range` 📖	mathematical	`MeasurableSet`	`Finset` `Finset.instMembership` `range` `restrict` `Set` `Set.instMembership` `Set.image` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	—	`Finset.mem_coe` `coe_range` `coe_restrict` `Set.mem_range_indicator`
`mk_le_mk` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set` `Set.instSingletonSet`	`MeasureTheory.SimpleFunc` `instLE` `Preorder.toLE` `Pi.hasLe`	—	—
`mk_lt_mk` 📖	mathematical	`MeasurableSet` `Set.preimage` `Set` `Set.instSingletonSet`	`MeasureTheory.SimpleFunc` `Preorder.toLT` `instPreorder` `Pi.preorder`	—	—
`monotone_approx` 📖	mathematical	—	`Monotone` `MeasureTheory.SimpleFunc` `Nat.instPreorder` `instPreorder` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `approx`	—	`Finset.sup_mono` `Finset.range_subset_range`
`monotone_eapprox` 📖	mathematical	—	`Monotone` `MeasureTheory.SimpleFunc` `ENNReal` `Nat.instPreorder` `instPreorder` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `eapprox`	—	`monotone_approx`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instMul`	—	—
`mul_eq_map₂` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instMul` `map` `pair`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instNeg`	—	—
`pair_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `pair`	—	—
`pair_preimage` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `pair` `SProd.sprod` `Set` `Set.instSProd` `Set.instInter`	—	—
`pair_preimage_singleton` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `pair` `Set` `Set.instSingletonSet` `Set.instInter`	—	`Set.singleton_prod_singleton` `pair_preimage`
`piecewise_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `piecewise` `Set` `Set.instMembership`	—	—
`piecewise_compl` 📖	mathematical	`MeasurableSet` `Compl.compl` `Set` `Set.instCompl`	`piecewise` `MeasurableSet.of_compl`	—	`coe_injective` `MeasurableSet.of_compl` `Set.piecewise_compl`
`piecewise_empty` 📖	mathematical	—	`piecewise` `Set` `Set.instEmptyCollection` `MeasurableSet.empty`	—	`coe_injective` `MeasurableSet.empty` `Set.piecewise_empty`
`piecewise_mono` 📖	mathematical	`MeasurableSet` `Preorder.toLE` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike`	`instLE` `piecewise`	—	`Set.piecewise_mono`
`piecewise_same` 📖	mathematical	`MeasurableSet`	`piecewise`	—	`coe_injective` `Set.piecewise_same`
`piecewise_univ` 📖	mathematical	—	`piecewise` `Set.univ` `MeasurableSet.univ`	—	`coe_injective` `MeasurableSet.univ` `Set.piecewise_univ`
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `hasNatPow` `Monoid.toNatPow`	—	—
`preimage_eq_empty_iff` 📖	mathematical	—	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `Set` `Set.instSingletonSet` `Set.instEmptyCollection` `Finset` `Finset.instMembership` `range`	—	`Set.preimage_singleton_eq_empty` `mem_range`
`range_comp_subset_range` 📖	mathematical	`Measurable`	`Finset` `Finset.instHasSubset` `range` `comp`	—	`Finset.coe_subset` `coe_range`
`range_const` 📖	mathematical	—	`range` `const` `Finset` `Finset.instSingleton`	—	`Finset.coe_injective` `coe_range` `Set.range_const` `Finset.coe_singleton`
`range_const_subset` 📖	mathematical	—	`Finset` `Finset.instHasSubset` `range` `const` `Finset.instSingleton`	—	`Finset.coe_subset` `coe_range` `Finset.coe_singleton`
`range_eq_empty_of_isEmpty` 📖	mathematical	—	`range` `Finset` `Finset.instEmptyCollection`	—	`Finset.ext`
`range_indicator` 📖	mathematical	`MeasurableSet` `Set.Nonempty`	`range` `piecewise` `const` `Finset` `Finset.instInsert` `Finset.instSingleton`	—	`coe_range` `Set.range_piecewise` `Set.image_congr` `Set.Nonempty.image_const` `Set.nonempty_compl` `Finset.coe_insert` `Finset.coe_singleton`
`range_map` 📖	mathematical	—	`range` `map` `Finset.image`	—	`Finset.coe_injective` `coe_range` `Set.range_comp` `Finset.coe_image`
`range_one` 📖	mathematical	—	`range` `MeasureTheory.SimpleFunc` `instOne` `Finset` `Finset.instSingleton`	—	`Finset.ext` `Set.range_one`
`range_zero` 📖	mathematical	—	`range` `MeasureTheory.SimpleFunc` `instZero` `Finset` `Finset.instSingleton`	—	`Finset.ext` `mem_range` `Set.range_zero` `Set.mem_singleton_iff` `Finset.mem_singleton`
`restrict_apply` 📖	mathematical	`MeasurableSet`	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `restrict` `Set.indicator`	—	`coe_restrict`
`restrict_const_lintegral` 📖	mathematical	`MeasurableSet`	`lintegral` `restrict` `ENNReal` `instZeroENNReal` `const` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike`	—	`restrict_lintegral_eq_lintegral_restrict` `const_lintegral_restrict`
`restrict_empty` 📖	mathematical	—	`restrict` `Set` `Set.instEmptyCollection` `MeasureTheory.SimpleFunc` `instZero`	—	`piecewise_empty`
`restrict_lintegral` 📖	mathematical	`MeasurableSet`	`lintegral` `restrict` `ENNReal` `instZeroENNReal` `Finset.sum` `ENNReal.instAddCommMonoid` `range` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.instInter` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet`	—	`lintegral_eq_of_subset` `restrict_apply` `Set.indicator_of_mem` `coe_restrict` `Set.indicator_of_notMem` `Finset.sum_congr` `forall_mem_range` `MulZeroClass.zero_mul` `restrict_preimage_singleton` `Set.inter_comm`
`restrict_lintegral_eq_lintegral_restrict` 📖	mathematical	`MeasurableSet`	`lintegral` `restrict` `ENNReal` `instZeroENNReal` `MeasureTheory.Measure.restrict`	—	`restrict_lintegral` `lintegral_restrict`
`restrict_mono` 📖	mathematical	`MeasureTheory.SimpleFunc` `instLE` `Preorder.toLE`	`restrict`	—	`coe_restrict` `Set.indicator_le_indicator` `restrict_of_not_measurable`
`restrict_of_not_measurable` 📖	mathematical	`MeasurableSet`	`restrict` `MeasureTheory.SimpleFunc` `instZero`	—	—
`restrict_preimage` 📖	mathematical	`MeasurableSet` `Set` `Set.instMembership`	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `restrict` `Set.instInter`	—	`coe_restrict` `Set.indicator_preimage_of_notMem` `Set.inter_comm`
`restrict_preimage_singleton` 📖	mathematical	`MeasurableSet`	`Set.preimage` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `restrict` `Set` `Set.instSingletonSet` `Set.instInter`	—	`restrict_preimage`
`restrict_univ` 📖	mathematical	—	`restrict` `Set.univ`	—	`piecewise_univ`
`seq_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `seq`	—	—
`simpleFunc_bot` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `instFunLike`	—	`measurableSet_fiber` `Set.exists_eq_const_of_preimage_singleton`
`simpleFunc_bot'` 📖	mathematical	—	`const` `Bot.bot` `MeasurableSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `MeasurableSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`ext` `simpleFunc_bot`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSMul`	—	—
`smul_const` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instSMul` `const`	—	`ext`
`smul_eq_map` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instSMul` `map`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSub`	—	—
`sum_eapproxDiff` 📖	mathematical	—	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `Finset.range` `ENNReal.ofNNReal` `DFunLike.coe` `MeasureTheory.SimpleFunc` `NNReal` `instFunLike` `eapproxDiff` `eapprox`	—	`Finset.sum_congr` `zero_add` `Finset.sum_singleton` `ENNReal.coe_toNNReal` `LT.lt.ne` `eapprox_lt_top` `Finset.sum_range_succ` `eapproxDiff.eq_2` `coe_map` `coe_sub` `Pi.sub_apply` `lt_of_le_of_lt` `tsub_le_iff_right` `ENNReal.instOrderedSub` `le_self_add` `ENNReal.instCanonicallyOrderedAdd` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `IsOrderedAddMonoid.toAddLeftMono` `ENNReal.instIsOrderedAddMonoid` `monotone_eapprox`
`sum_measure_preimage_singleton` 📖	mathematical	—	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`MeasureTheory.sum_measure_preimage_singleton` `measurableSet_fiber`
`sum_range_measure_preimage_singleton` 📖	mathematical	—	`Finset.sum` `ENNReal` `ENNReal.instAddCommMonoid` `range` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `instFunLike` `Set.instSingletonSet` `Set.univ`	—	`sum_measure_preimage_singleton` `coe_range` `Set.preimage_range`
`sup_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `instSup`	—	—
`sup_eq_map₂` 📖	mathematical	—	`MeasureTheory.SimpleFunc` `instSup` `map` `pair`	—	—
`support_eq` 📖	mathematical	—	`Function.support` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `Set.iUnion` `Finset` `Finset.instMembership` `Finset.filter` `range` `Set.preimage` `Set` `Set.instSingletonSet`	—	`Set.ext` `Set.iUnion_congr_Prop`
`support_indicator` 📖	mathematical	`MeasurableSet`	`Function.support` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `piecewise` `const` `Set` `Set.instInter`	—	`Set.support_indicator`
`tendsto_eapprox` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.Tendsto` `DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `eapprox` `Filter.atTop` `Nat.instPreorder` `nhds` `ENNReal.instTopologicalSpace`	—	`iSup_coe_eapprox` `iSup_apply` `tendsto_atTop_iSup` `LinearOrder.supConvergenceClass` `ENNReal.instOrderTopology` `monotone_eapprox`
`tsum_eapproxDiff` 📖	mathematical	`Measurable` `ENNReal` `ENNReal.measurableSpace`	`tsum` `ENNReal.instAddCommMonoid` `ENNReal.instTopologicalSpace` `ENNReal.ofNNReal` `DFunLike.coe` `MeasureTheory.SimpleFunc` `NNReal` `instFunLike` `eapproxDiff` `SummationFilter.unconditional`	—	`ENNReal.tsum_eq_iSup_nat'` `Filter.tendsto_add_atTop_nat` `sum_eapproxDiff` `iSup_eapprox_apply`
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—
`zero_lintegral` 📖	mathematical	—	`lintegral` `MeasureTheory.SimpleFunc` `ENNReal` `instZero` `instZeroENNReal`	—	`IsScalarTower.right` `Algebra.to_smulCommClass` `LinearMap.ext_iff` `LinearMap.map_zero`
`zpow_apply` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.SimpleFunc` `instFunLike` `hasIntPow` `DivInvMonoid.toZPow`	—	—

MeasureTheory.SimpleFunc.FinMeasSupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp` `AddZero.toZero` `AddZeroClass.toAddZero`	`MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instAdd` `AddZero.toAdd`	—	`MeasureTheory.SimpleFunc.add_eq_map₂` `map₂` `zero_add`
`iff_lintegral_lt_top` 📖	mathematical	`Filter.Eventually` `ENNReal` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`MeasureTheory.SimpleFunc.FinMeasSupp` `instZeroENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.SimpleFunc.lintegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `lintegral_lt_top` `of_lintegral_ne_top` `LT.lt.ne`
`lintegral_lt_top` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp` `ENNReal` `instZeroENNReal` `Filter.Eventually` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass`	`Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.SimpleFunc.lintegral`	—	`MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.sum_lt_top` `eq_or_ne` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `ENNReal.mul_lt_top` `Ne.lt_top` `MeasureTheory.SimpleFunc.finMeasSupp_iff`
`map` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp`	`MeasureTheory.SimpleFunc.map`	—	`lt_of_le_of_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_comp_subset`
`map_iff` 📖	mathematical	—	`MeasureTheory.SimpleFunc.FinMeasSupp` `MeasureTheory.SimpleFunc.map`	—	`of_map` `map`
`map₂` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp`	`MeasureTheory.SimpleFunc.map` `MeasureTheory.SimpleFunc.pair`	—	`map` `pair`
`meas_preimage_singleton_ne_zero` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp`	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `Set.preimage` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike` `Set.instSingletonSet` `Top.top` `instTopENNReal`	—	`MeasureTheory.SimpleFunc.finMeasSupp_iff`
`mul` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp` `MulZeroClass.toZero`	`MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instMul` `MulZeroClass.toMul`	—	`MeasureTheory.SimpleFunc.mul_eq_map₂` `map₂` `MulZeroClass.zero_mul`
`of_lintegral_ne_top` 📖	mathematical	—	`MeasureTheory.SimpleFunc.FinMeasSupp` `ENNReal` `instZeroENNReal`	—	`MeasureTheory.SimpleFunc.finMeasSupp_iff` `ENNReal.lt_top_of_mul_ne_top_right` `LT.lt.ne` `ENNReal.lt_top_of_sum_ne_top` `MeasureTheory.SimpleFunc.lintegral_eq_of_subset'` `Finset.subset_insert` `Finset.mem_insert_self`
`of_map` 📖	—	`MeasureTheory.SimpleFunc.FinMeasSupp` `MeasureTheory.SimpleFunc.map`	—	—	`lt_of_le_of_lt` `MeasureTheory.measure_mono` `MeasureTheory.Measure.instOuterMeasureClass` `Function.support_subset_comp`
`pair` 📖	mathematical	`MeasureTheory.SimpleFunc.FinMeasSupp`	`Prod.instZero` `MeasureTheory.SimpleFunc.pair`	—	`Function.support_prodMk` `MeasureTheory.measure_union_le` `MeasureTheory.Measure.instOuterMeasureClass` `ENNReal.add_lt_top`

---

← Back to Index