Set

📁 Source: Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Statistics

Metric	Count
Definitions `LpToLpRestrictCLM`	1
Theorems `integral_pos_of_hasCompactSupport_nonneg_nonzero`, `setIntegral_map`, `measure_le_integral`, `simpleFunc_mul`, `simpleFunc_mul'`, `LpToLpRestrictCLM_coeFn`, `Lp_toLp_restrict_add`, `Lp_toLp_restrict_smul`, `setIntegral_image_emb`, `setIntegral_preimage_emb`, `continuous_setIntegral`, `hasSum_integral_iUnion`, `hasSum_integral_iUnion_ae`, `integrableOn_iUnion_of_summable_integral_norm`, `integrableOn_iUnion_of_summable_norm_restrict`, `integrable_of_summable_norm_restrict`, `integral_Icc_eq_integral_Ico`, `integral_Icc_eq_integral_Ico'`, `integral_Icc_eq_integral_Ioc`, `integral_Icc_eq_integral_Ioc'`, `integral_Icc_eq_integral_Ioo`, `integral_Icc_eq_integral_Ioo'`, `integral_Ici_eq_integral_Ioi`, `integral_Ici_eq_integral_Ioi'`, `integral_Ico_eq_integral_Ioc`, `integral_Ico_eq_integral_Ioo`, `integral_Ico_eq_integral_Ioo'`, `integral_Iic_eq_integral_Iio`, `integral_Iic_eq_integral_Iio'`, `integral_Ioc_eq_integral_Ioo`, `integral_Ioc_eq_integral_Ioo'`, `integral_add_compl`, `integral_add_compl₀`, `integral_biUnion_eq_sum_powerset`, `integral_biUnion_finset`, `integral_diff`, `integral_eq_setIntegral`, `integral_iUnion`, `integral_iUnion_ae`, `integral_iUnion_fintype`, `integral_indicator`, `integral_indicatorConstLp`, `integral_indicator_const`, `integral_indicator_one`, `integral_indicator₀`, `integral_integral_indicator`, `integral_inter_add_diff`, `integral_inter_add_diff₀`, `integral_le_measure`, `integral_norm_eq_pos_sub_neg`, `integral_piecewise`, `integral_union_ae`, `integral_union_eq_left_of_ae`, `integral_union_eq_left_of_ae_aux`, `integral_union_eq_left_of_forall`, `integral_union_eq_left_of_forall₀`, `measureReal_biUnion_eq_sum_powerset`, `norm_Lp_toLp_restrict_le`, `norm_integral_sub_setIntegral_le`, `norm_setIntegral_le_of_norm_le_const`, `norm_setIntegral_le_of_norm_le_const_ae`, `norm_setIntegral_le_of_norm_le_const_ae'`, `ofReal_setIntegral_one`, `ofReal_setIntegral_one_of_measure_ne_top`, `setIntegral_compl`, `setIntegral_compl₀`, `setIntegral_congr_ae`, `setIntegral_congr_ae₀`, `setIntegral_congr_fun`, `setIntegral_congr_fun₀`, `setIntegral_congr_set`, `setIntegral_const`, `setIntegral_diff`, `setIntegral_diff₀`, `setIntegral_empty`, `setIntegral_eq_integral_of_ae_compl_eq_zero`, `setIntegral_eq_integral_of_forall_compl_eq_zero`, `setIntegral_eq_of_subset_of_ae_diff_eq_zero`, `setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux`, `setIntegral_eq_of_subset_of_forall_diff_eq_zero`, `setIntegral_eq_zero_iff_of_nonneg_ae`, `setIntegral_eq_zero_of_ae_eq_zero`, `setIntegral_eq_zero_of_forall_eq_zero`, `setIntegral_ge_of_const_le`, `setIntegral_ge_of_const_le_real`, `setIntegral_gt_gt`, `setIntegral_indicator`, `setIntegral_indicatorConstLp`, `setIntegral_le_integral`, `setIntegral_le_nonneg`, `setIntegral_map`, `setIntegral_map_equiv`, `setIntegral_mono`, `setIntegral_mono_ae`, `setIntegral_mono_ae_restrict`, `setIntegral_mono_on`, `setIntegral_mono_on_ae`, `setIntegral_mono_on_ae₀`, `setIntegral_mono_on₀`, `setIntegral_mono_set`, `setIntegral_neg_eq_setIntegral_nonpos`, `setIntegral_nonneg`, `setIntegral_nonneg_ae`, `setIntegral_nonneg_of_ae`, `setIntegral_nonneg_of_ae_restrict`, `setIntegral_nonpos`, `setIntegral_nonpos_ae`, `setIntegral_nonpos_le`, `setIntegral_nonpos_of_ae`, `setIntegral_nonpos_of_ae_restrict`, `setIntegral_one_eq_measureReal`, `setIntegral_pos_iff_support_of_nonneg_ae`, `setIntegral_support`, `setIntegral_trim`, `setIntegral_tsupport`, `setIntegral_union`, `setIntegral_union₀`, `setIntegral_univ`, `tendsto_setIntegral_of_antitone`, `tendsto_setIntegral_of_monotone`, `tendsto_setIntegral_of_monotone₀`, `setIntegral_map`, `continuousOn_integral_bilinear_of_locally_integrable_of_compact_support`, `continuousOn_integral_of_compact_support`, `continuous_parametric_integral_of_continuous`, `measure_le_lintegral_thickenedIndicator`, `measure_le_lintegral_thickenedIndicatorAux`	127
Total	128

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`integral_pos_of_hasCompactSupport_nonneg_nonzero` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `HasCompactSupport` `Real.instZero` `Pi.hasLe` `Real.instLE` `Pi.instZero`	`Real` `Real.instLT` `Real.instZero` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField`	—	`MeasureTheory.integral_pos_of_integrable_nonneg_nonzero` `integrable_of_hasCompactSupport`

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`setIntegral_map` 📖	mathematical	`MeasurableEmbedding`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `MeasureTheory.Measure.map` `Set.preimage`	—	`restrict_map` `integral_map`

MeasureTheory

Definitions

Name	Category	Theorems
`LpToLpRestrictCLM` 📖	CompOp	1 math math: `LpToLpRestrictCLM_coeFn`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`LpToLpRestrictCLM_coeFn` 📖	mathematical	—	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `DFunLike.coe` `ContinuousLinearMap` `Ring.toSemiring` `NormedRing.toRing` `RingHom.id` `Semiring.toNonAssocSemiring` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `Lp.instNormedAddCommGroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Lp.instModule` `ContinuousLinearMap.funLike` `LpToLpRestrictCLM`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MemLp.coeFn_toLp` `MemLp.restrict` `Lp.memLp`
`Lp_toLp_restrict_add` 📖	mathematical	—	`MemLp.toLp` `Measure.restrict` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `AddSubgroup.add` `MemLp.restrict` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Lp.memLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Lp.ext` `MemLp.restrict` `Lp.memLp` `Filter.Eventually.mp` `Measure.instOuterMeasureClass` `ae_restrict_of_ae` `Lp.coeFn_add` `MemLp.coeFn_toLp` `Filter.Eventually.mono` `Pi.add_apply`
`Lp_toLp_restrict_smul` 📖	mathematical	—	`MemLp.toLp` `Measure.restrict` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddSubgroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `AddSubgroup.toAddCommGroup` `AEEqFun.instAddCommGroup` `NormedAddCommGroup.toAddCommGroup` `Lp.instModule` `MemLp.restrict` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Lp.memLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `Lp.ext` `MemLp.restrict` `Lp.memLp` `Filter.Eventually.mp` `Measure.instOuterMeasureClass` `ae_restrict_of_ae` `Lp.coeFn_smul` `MemLp.coeFn_toLp` `Filter.Eventually.mono`
`continuous_setIntegral` 📖	mathematical	—	`Continuous` `AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `ENNReal` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `Lp.instNormedAddCommGroup` `fact_one_le_one_ennreal` `integral` `Measure.restrict` `AEEqFun.cast`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `le_rfl` `NormedSpace.toIsBoundedSMul` `integral_congr_ae` `LpToLpRestrictCLM_coeFn` `fact_one_le_one_ennreal` `Continuous.comp` `continuous_integral` `ContinuousLinearMap.continuous`
`hasSum_integral_iUnion` 📖	mathematical	`MeasurableSet` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Set.iUnion` `SummationFilter.unconditional`	—	`hasSum_integral_iUnion_ae` `MeasurableSet.nullMeasurableSet` `Pairwise.mono` `Disjoint.aedisjoint`
`hasSum_integral_iUnion_ae` 📖	mathematical	`NullMeasurableSet` `Pairwise` `Function.onFun` `Set` `AEDisjoint` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`HasSum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Set.iUnion` `SummationFilter.unconditional`	—	`Measure.restrict_iUnion_ae` `hasSum_integral_measure`
`integrableOn_iUnion_of_summable_integral_norm` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Summable` `Real` `Real.instAddCommMonoid` `Real.pseudoMetricSpace` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Norm.norm` `NormedAddCommGroup.toNorm` `SummationFilter.unconditional`	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	—	`AEStronglyMeasurable.iUnion` `PseudoEMetricSpace.pseudoMetrizableSpace` `LE.le.trans_lt` `lintegral_iUnion_le` `lintegral_coe_eq_integral` `Integrable.norm` `tsum_congr` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `integral_nonneg` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `NNReal.coe_nonneg` `NNReal.summable_coe` `ENNReal.tsum_coe_eq` `Summable.hasSum` `ENNReal.coe_nnreal_eq` `ENNReal.ofReal_lt_top`
`integrableOn_iUnion_of_summable_norm_restrict` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Norm.norm` `ContinuousMap` `Set.Elem` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `ContinuousMap.instCompactSpaceElemCoeCompacts` `ContinuousMap.restrict` `Measure.real` `SummationFilter.unconditional`	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `Set.iUnion` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike`	—	`ContinuousMap.instCompactSpaceElemCoeCompacts` `integrableOn_iUnion_of_summable_integral_norm` `ContinuousOn.integrableOn_compact` `BorelSpace.opensMeasurable` `isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `TopologicalSpace.Compacts.isCompact` `Continuous.continuousOn` `ContinuousMapClass.map_continuous` `ContinuousMap.instContinuousMapClass` `Summable.of_nonneg_of_le` `integral_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `norm_nonneg` `Real.norm_of_nonneg` `norm_setIntegral_le_of_norm_le_const` `IsCompact.measure_lt_top` `ContinuousMap.norm_coe_le_norm` `norm_norm`
`integrable_of_summable_norm_restrict` 📖	mathematical	`Summable` `Real` `Real.instAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instMul` `Norm.norm` `ContinuousMap` `Set.Elem` `SetLike.coe` `TopologicalSpace.Compacts` `TopologicalSpace.Compacts.instSetLike` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ContinuousMap.instNorm` `ContinuousMap.instCompactSpaceElemCoeCompacts` `ContinuousMap.restrict` `Measure.real` `SummationFilter.unconditional` `Set.iUnion` `Set.univ`	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	`ContinuousMap.instCompactSpaceElemCoeCompacts` `integrableOn_iUnion_of_summable_norm_restrict`
`integral_Icc_eq_integral_Ico` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ico`	—	`integral_Icc_eq_integral_Ico'` `NoAtoms.measure_singleton`
`integral_Icc_eq_integral_Ico'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ico`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ico_ae_eq_Icc'`
`integral_Icc_eq_integral_Ioc` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ioc`	—	`integral_Icc_eq_integral_Ioc'` `NoAtoms.measure_singleton`
`integral_Icc_eq_integral_Ioc'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ioc`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ioc_ae_eq_Icc'`
`integral_Icc_eq_integral_Ioo` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ioo`	—	`integral_Icc_eq_integral_Ico` `integral_Ico_eq_integral_Ioo`
`integral_Icc_eq_integral_Ioo'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Icc` `PartialOrder.toPreorder` `Set.Ioo`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ioo_ae_eq_Icc'`
`integral_Ici_eq_integral_Ioi` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Ici` `PartialOrder.toPreorder` `Set.Ioi`	—	`integral_Ici_eq_integral_Ioi'` `NoAtoms.measure_singleton`
`integral_Ici_eq_integral_Ioi'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Ici` `PartialOrder.toPreorder` `Set.Ioi`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ioi_ae_eq_Ici'`
`integral_Ico_eq_integral_Ioc` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Ico` `PartialOrder.toPreorder` `Set.Ioc`	—	`integral_Ico_eq_integral_Ioo` `integral_Ioc_eq_integral_Ioo`
`integral_Ico_eq_integral_Ioo` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Ico` `PartialOrder.toPreorder` `Set.Ioo`	—	`integral_Ico_eq_integral_Ioo'` `NoAtoms.measure_singleton`
`integral_Ico_eq_integral_Ioo'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Ico` `PartialOrder.toPreorder` `Set.Ioo`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ioo_ae_eq_Ico'`
`integral_Iic_eq_integral_Iio` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Iic` `PartialOrder.toPreorder` `Set.Iio`	—	`integral_Iic_eq_integral_Iio'` `NoAtoms.measure_singleton`
`integral_Iic_eq_integral_Iio'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Iic` `PartialOrder.toPreorder` `Set.Iio`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Iio_ae_eq_Iic'`
`integral_Ioc_eq_integral_Ioo` 📖	mathematical	—	`integral` `Measure.restrict` `Set.Ioc` `PartialOrder.toPreorder` `Set.Ioo`	—	`integral_Ioc_eq_integral_Ioo'` `NoAtoms.measure_singleton`
`integral_Ioc_eq_integral_Ioo'` 📖	mathematical	`DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike` `Set.instSingletonSet` `instZeroENNReal`	`integral` `Measure.restrict` `Set.Ioc` `PartialOrder.toPreorder` `Set.Ioo`	—	`setIntegral_congr_set` `Filter.EventuallyEq.symm` `Measure.instOuterMeasureClass` `Ioo_ae_eq_Ioc'`
`integral_add_compl` 📖	mathematical	`MeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl`	—	`integral_add_compl₀` `MeasurableSet.nullMeasurableSet`
`integral_add_compl₀` 📖	mathematical	`NullMeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl`	—	`setIntegral_union₀` `Disjoint.aedisjoint` `disjoint_compl_right` `NullMeasurableSet.compl` `Integrable.integrableOn` `Set.union_compl_self` `setIntegral_univ`
`integral_biUnion_eq_sum_powerset` 📖	mathematical	`MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.filter` `Finset.Nonempty` `Finset.decidableNonempty` `Finset.powerset` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `NormedSpace.toModule` `Real.normedField` `Monoid.toPow` `Real.instNeg` `Real.instOne` `Finset.card` `Set.iInter`	—	`Finset.sum_congr` `NormedSpace.toNormSMulClass` `smulCommClass_self` `integral_indicator` `Finset.measurableSet_biUnion` `Finset.measurableSet_biInter` `integral_finset_sum` `integrable_indicator_iff` `Integrable.smul` `NormedSpace.toIsBoundedSMul` `IntegrableOn.mono` `Set.biInter_subset_of_mem` `le_rfl` `Set.indicator_smul_apply` `Nat.cast_one` `Int.cast_smul_eq_zsmul` `Finset.indicator_biUnion_eq_sum_powerset`
`integral_biUnion_finset` 📖	mathematical	`MeasurableSet` `Set.Pairwise` `SetLike.coe` `Finset` `Finset.instSetLike` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Finset.induction_on` `Set.iUnion_congr_Prop` `Set.iUnion_of_empty` `instIsEmptyFalse` `Set.iUnion_empty` `Measure.restrict_empty` `integral_zero_measure` `Finset.set_biUnion_insert` `setIntegral_union` `Finset.coe_insert` `Finset.measurableSet_biUnion` `integrableOn_finset_iUnion` `PseudoEMetricSpace.pseudoMetrizableSpace` `Finset.sum_insert`
`integral_diff` 📖	mathematical	`MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set` `Set.instHasSubset`	`integral` `Measure.restrict` `Set` `Set.instSDiff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`setIntegral_diff`
`integral_eq_setIntegral` 📖	mathematical	`Filter.Eventually` `Set` `Set.instMembership` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_univ` `setIntegral_congr_set` `ae_eq_univ`
`integral_iUnion` 📖	mathematical	`MeasurableSet` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`integral` `Measure.restrict` `Set.iUnion` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_iUnion`
`integral_iUnion_ae` 📖	mathematical	`NullMeasurableSet` `Pairwise` `Function.onFun` `Set` `AEDisjoint` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`integral` `Measure.restrict` `Set.iUnion` `tsum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SummationFilter.unconditional`	—	`HasSum.tsum_eq` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `SummationFilter.instNeBotUnconditional` `hasSum_integral_iUnion_ae`
`integral_iUnion_fintype` 📖	mathematical	`MeasurableSet` `Pairwise` `Function.onFun` `Set` `Disjoint` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set.iUnion` `Finset.sum` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Finset.univ`	—	`Set.iUnion_congr_Prop` `Set.iUnion_true` `integral_biUnion_finset` `Finset.coe_univ`
`integral_indicator` 📖	mathematical	`MeasurableSet`	`integral` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Measure.restrict`	—	`integral_add_compl` `IntegrableOn.integrable_indicator` `integral_congr_ae` `indicator_ae_eq_restrict` `indicator_ae_eq_restrict_compl` `integral_zero` `add_zero` `integral_undef` `integrable_indicator_iff`
`integral_indicatorConstLp` 📖	mathematical	`MeasurableSet`	`integral` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `indicatorConstLp` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Measure.real`	—	`setIntegral_univ` `setIntegral_indicatorConstLp` `MeasurableSet.univ` `Set.inter_univ`
`integral_indicator_const` 📖	mathematical	`MeasurableSet`	`integral` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Measure.real`	—	`integral_indicator` `setIntegral_const`
`integral_indicator_one` 📖	mathematical	`MeasurableSet`	`integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Set.indicator` `Real.instZero` `Pi.instOne` `Real.instOne` `Measure.real`	—	`integral_indicator_const` `Real.instCompleteSpace` `smul_eq_mul` `mul_one`
`integral_indicator₀` 📖	mathematical	`NullMeasurableSet`	`integral` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Measure.restrict`	—	`integral_congr_ae` `indicator_ae_eq_of_ae_eq_set` `NullMeasurableSet.toMeasurable_ae_eq` `integral_indicator` `measurableSet_toMeasurable` `Measure.restrict_congr_set`
`integral_integral_indicator` 📖	mathematical	`MeasurableSet`	`integral` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Measure.restrict`	—	`integral_indicator` `integral_indicator₂`
`integral_inter_add_diff` 📖	mathematical	`MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Set` `Set.instInter` `Set.instSDiff`	—	`integral_inter_add_diff₀` `MeasurableSet.nullMeasurableSet`
`integral_inter_add_diff₀` 📖	mathematical	`NullMeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `integral` `Measure.restrict` `Set` `Set.instInter` `Set.instSDiff`	—	`Measure.restrict_inter_add_diff₀` `integral_add_measure` `Integrable.mono_measure` `Measure.restrict_mono` `Set.inter_subset_left` `le_rfl` `Set.diff_subset`
`integral_le_measure` 📖	mathematical	`Real` `Real.instLE` `Real.instOne` `Real.instZero`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `ENNReal.ofReal` `integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike`	—	`Integrable.pos_part` `ENNReal.ofReal_le_ofReal` `integral_mono` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `le_max_left` `LE.le.trans` `ofReal_integral_eq_lintegral_ofReal` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass` `le_max_right` `lintegral_le_meas` `ENNReal.ofReal_le_of_le_toReal` `Real.instZeroLEOneClass` `le_trans` `instReflLe` `zero_le_one` `ENNReal.ofReal_max` `ENNReal.ofReal_zero` `sup_of_le_left` `ENNReal.instCanonicallyOrderedAdd` `integral_undef`
`integral_norm_eq_pos_sub_neg` 📖	mathematical	`Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Norm.norm` `Real.norm` `Real.instSub` `Measure.restrict` `setOf` `Real.instLE` `Real.instZero`	—	`AEStronglyMeasurable.nullMeasurableSet_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace` `aestronglyMeasurable_const` `integral_add_compl₀` `Integrable.norm` `setIntegral_congr_fun₀` `Real.norm_eq_abs` `abs_eq_self` `integral_neg` `NullMeasurableSet.compl` `abs_eq_neg_self` `le_of_not_gt` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.cast_zero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_zero` `Mathlib.Tactic.Ring.sub_pf` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Tactic.Linarith.add_neg` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `Real.instIsOrderedRing` `lt_of_not_ge` `Set.notMem_setOf_iff` `Set.mem_compl_iff` `setIntegral_neg_eq_setIntegral_nonpos` `Set.compl_setOf`
`integral_piecewise` 📖	mathematical	`MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Compl.compl` `Set` `Set.instCompl`	`integral` `Set.piecewise` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl`	—	`Set.indicator_add_compl_eq_piecewise` `integral_add'` `IntegrableOn.integrable_indicator` `MeasurableSet.compl` `integral_indicator`
`integral_union_ae` 📖	mathematical	`AEDisjoint` `NullMeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set` `Set.instUnion` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`setIntegral_union₀`
`integral_union_eq_left_of_ae` 📖	mathematical	`Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict`	`integral` `Measure.restrict` `Set` `Set.instUnion`	—	`Measure.instOuterMeasureClass` `IntegrableOn.congr_fun_ae` `integrableOn_zero` `Filter.EventuallyEq.symm` `integral_congr_ae` `integral_union_eq_left_of_ae_aux` `Filter.mp_mem` `ae_mono` `Measure.restrict_mono` `Set.subset_union_right` `le_rfl` `Filter.univ_mem'` `Set.subset_union_left` `integral_undef` `PseudoEMetricSpace.pseudoMetrizableSpace`
`integral_union_eq_left_of_ae_aux` 📖	mathematical	`Filter.Eventually` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set` `Set.instUnion`	`integral` `Measure.restrict` `Set` `Set.instUnion`	—	`Measure.instOuterMeasureClass` `StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasurableSingletonClass.measurableSet_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `IntegrableOn.mono` `Set.subset_union_left` `le_rfl` `setIntegral_eq_zero_of_forall_eq_zero` `integral_inter_add_diff` `zero_add` `Set.union_diff_distrib` `Set.union_comm` `setIntegral_congr_set` `union_ae_eq_right` `measure_mono_null` `Set.diff_subset` `measure_eq_zero_iff_ae_notMem` `Filter.mp_mem` `ae_imp_of_ae_restrict` `Filter.univ_mem'`
`integral_union_eq_left_of_forall` 📖	mathematical	`MeasurableSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `Measure.restrict` `Set` `Set.instUnion`	—	`integral_union_eq_left_of_forall₀` `MeasurableSet.nullMeasurableSet`
`integral_union_eq_left_of_forall₀` 📖	mathematical	`NullMeasurableSet` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `Measure.restrict` `Set` `Set.instUnion`	—	`integral_union_eq_left_of_ae` `Measure.instOuterMeasureClass` `ae_restrict_iff'₀` `Filter.Eventually.of_forall`
`measureReal_biUnion_eq_sum_powerset` 📖	mathematical	`MeasurableSet`	`Measure.real` `Set.iUnion` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Finset.sum` `Real` `Real.instAddCommMonoid` `Finset.filter` `Finset.Nonempty` `Finset.decidableNonempty` `Finset.powerset` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNeg` `Real.instOne` `Finset.card` `Set.iInter`	—	`Finset.sum_congr` `integral_biUnion_eq_sum_powerset` `enorm_one` `NormedDivisionRing.to_normOneClass` `NeZero.charZero_one` `ENNReal.instCharZero` `Ne.lt_top`
`norm_Lp_toLp_restrict_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `AEEqFun` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.restrict` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `Lp.instNorm` `MemLp.toLp` `AEEqFun.cast` `MemLp.restrict` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Lp.memLp`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `MemLp.restrict` `Lp.memLp` `Lp.norm_def` `eLpNorm_congr_ae` `MemLp.coeFn_toLp` `ENNReal.toReal_mono` `Lp.eLpNorm_ne_top` `eLpNorm_mono_measure` `Measure.restrict_le_self`
`norm_integral_sub_setIntegral_le` 📖	mathematical	`Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `MeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `integral` `Measure.restrict` `Real.instMul` `Measure.real` `Compl.compl` `Set` `Set.instCompl`	—	`Measure.instOuterMeasureClass` `sub_eq_iff_eq_add` `add_comm` `integral_add_compl` `integral_mono_ae` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Integrable.restrict` `Integrable.norm` `integrable_const` `isFiniteMeasureRestrict` `ae_restrict_of_ae` `setIntegral_const` `Real.instCompleteSpace` `smul_eq_mul` `le_trans` `norm_integral_le_integral_norm`
`norm_setIntegral_le_of_norm_le_const` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `integral` `Measure.restrict` `Real.instMul` `Measure.real`	—	`norm_setIntegral_le_of_norm_le_const_ae'` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`norm_setIntegral_le_of_norm_le_const_ae` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal` `Filter.Eventually` `Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `ae` `Measure.instOuterMeasureClass` `Measure.restrict`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `integral` `Measure.restrict` `Real.instMul` `Measure.real`	—	`Measure.instOuterMeasureClass` `measureReal_restrict_apply` `Set.univ_inter` `norm_integral_le_of_norm_le_const` `Measure.restrict_apply_univ`
`norm_setIntegral_le_of_norm_le_const_ae'` 📖	mathematical	`ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal` `Filter.Eventually` `ae` `Measure.instOuterMeasureClass`	`Real` `Real.instLE` `Norm.norm` `NormedAddCommGroup.toNorm` `integral` `Measure.restrict` `Real.instMul` `Measure.real`	—	`Measure.instOuterMeasureClass` `norm_setIntegral_le_of_norm_le_const_ae` `Filter.mp_mem` `Filter.univ_mem'` `StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `StronglyMeasurable.norm` `measurableSet_Iic` `BorelSpace.opensMeasurable` `instClosedIicTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `ae_restrict_iff` `integral_non_aestronglyMeasurable` `frequently_ae_mem_iff` `Mathlib.Tactic.Contrapose.contrapose₄` `Measure.restrict_eq_zero` `Filter.Frequently.exists` `Filter.Frequently.and_eventually` `LE.le.trans` `norm_nonneg` `norm_zero` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `measureReal_nonneg`
`ofReal_setIntegral_one` 📖	mathematical	—	`ENNReal.ofReal` `integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instOne` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike`	—	`ofReal_setIntegral_one_of_measure_ne_top` `measure_ne_top`
`ofReal_setIntegral_one_of_measure_ne_top` 📖	mathematical	`ENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Top.top` `instTopENNReal`	`ENNReal.ofReal` `integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instOne` `DFunLike.coe` `Measure` `Set` `ENNReal` `Measure.instFunLike`	—	`NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `CStarRing.norm_of_mem_unitary` `instCStarRingReal` `Real.instNontrivial` `SubmonoidClass.toOneMemClass` `Submonoid.instSubmonoidClass` `integral_const` `Real.instCompleteSpace` `Measure.restrict_apply` `Set.univ_inter` `mul_one` `ENNReal.ofReal_toReal` `lintegral_const` `one_mul` `setLIntegral_one`
`setIntegral_compl` 📖	mathematical	`MeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`setIntegral_compl₀` `MeasurableSet.nullMeasurableSet`
`setIntegral_compl₀` 📖	mathematical	`NullMeasurableSet` `Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Compl.compl` `Set` `Set.instCompl` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`integral_add_compl₀` `add_sub_cancel_left`
`setIntegral_congr_ae` 📖	mathematical	`MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_congr_ae` `ae_restrict_iff'`
`setIntegral_congr_ae₀` 📖	mathematical	`NullMeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_congr_ae` `ae_restrict_iff'₀`
`setIntegral_congr_fun` 📖	mathematical	`MeasurableSet` `Set.EqOn`	`integral` `Measure.restrict`	—	`setIntegral_congr_ae` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_congr_fun₀` 📖	mathematical	`NullMeasurableSet` `Set.EqOn`	`integral` `Measure.restrict`	—	`setIntegral_congr_ae₀` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_congr_set` 📖	mathematical	`Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `Measure.restrict_congr_set`
`setIntegral_const` 📖	mathematical	—	`integral` `Measure.restrict` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Measure.real`	—	`integral_const` `measureReal_restrict_apply_univ`
`setIntegral_diff` 📖	mathematical	`MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set` `Set.instHasSubset`	`integral` `Measure.restrict` `Set` `Set.instSDiff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`setIntegral_diff₀` `MeasurableSet.nullMeasurableSet`
`setIntegral_diff₀` 📖	mathematical	`NullMeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set` `Set.instHasSubset`	`integral` `Measure.restrict` `Set` `Set.instSDiff` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup`	—	`eq_sub_iff_add_eq` `setIntegral_union₀` `Disjoint.aedisjoint` `disjoint_sdiff_self_left` `IntegrableOn.mono_set` `Set.diff_subset` `Set.diff_union_of_subset`
`setIntegral_empty` 📖	mathematical	—	`integral` `Measure.restrict` `Set` `Set.instEmptyCollection` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.restrict_empty` `integral_zero_measure`
`setIntegral_eq_integral_of_ae_compl_eq_zero` 📖	mathematical	`Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_univ` `setIntegral_eq_of_subset_of_ae_diff_eq_zero` `nullMeasurableSet_univ` `Set.subset_univ` `Filter.mp_mem` `Filter.univ_mem'`
`setIntegral_eq_integral_of_forall_compl_eq_zero` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `Measure.restrict`	—	`setIntegral_eq_integral_of_ae_compl_eq_zero` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_eq_of_subset_of_ae_diff_eq_zero` 📖	mathematical	`NullMeasurableSet` `Set` `Set.instHasSubset` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_congr_ae` `setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux` `Filter.mp_mem` `ae_imp_of_ae_restrict` `Filter.univ_mem'` `Integrable.congr` `ae_restrict_of_ae_restrict_of_subset` `Filter.EventuallyEq.symm` `IntegrableOn.of_ae_diff_eq_zero` `PseudoEMetricSpace.pseudoMetrizableSpace` `integral_undef`
`setIntegral_eq_of_subset_of_ae_diff_eq_zero_aux` 📖	mathematical	`Set` `Set.instHasSubset` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `StronglyMeasurable.measurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `MeasurableSingletonClass.measurableSet_singleton` `OpensMeasurableSpace.toMeasurableSingletonClass` `BorelSpace.opensMeasurable` `T5Space.toT1Space` `T6Space.toT5Space` `instT6SpaceOfMetrizableSpace` `EMetricSpace.metrizableSpace` `integral_inter_add_diff` `setIntegral_eq_zero_of_forall_eq_zero` `zero_add` `setIntegral_congr_set` `Filter.mp_mem` `Filter.univ_mem'` `IntegrableOn.mono` `le_rfl`
`setIntegral_eq_of_subset_of_forall_diff_eq_zero` 📖	mathematical	`MeasurableSet` `Set` `Set.instHasSubset` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `Measure.restrict`	—	`setIntegral_eq_of_subset_of_ae_diff_eq_zero` `MeasurableSet.nullMeasurableSet` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_eq_zero_iff_of_nonneg_ae` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `Real.instZero` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instZero` `Filter.EventuallyEq` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero`	—	`Measure.instOuterMeasureClass` `integral_eq_zero_iff_of_nonneg_ae`
`setIntegral_eq_zero_of_ae_eq_zero` 📖	mathematical	`Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`Measure.instOuterMeasureClass` `integral_eq_zero_of_ae` `Filter.EventuallyEq.eq_1` `ae_restrict_iff` `StronglyMeasurable.measurableSet_eq_fun` `EMetricSpace.metrizableSpace` `stronglyMeasurable_zero` `Filter.mp_mem` `ae_imp_of_ae_restrict` `Filter.univ_mem'` `integral_congr_ae` `integral_undef` `Mathlib.Tactic.Contrapose.contrapose₄`
`setIntegral_eq_zero_of_forall_eq_zero` 📖	mathematical	`NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`integral` `Measure.restrict` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`setIntegral_eq_zero_of_ae_eq_zero` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_ge_of_const_le` 📖	mathematical	`MeasurableSet` `Preorder.toLE` `PartialOrder.toPreorder` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Preorder.toLE` `PartialOrder.toPreorder` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Measure.real` `integral` `Measure.restrict`	—	`setIntegral_const` `setIntegral_mono_on` `integrableOn_const` `enorm_ne_top`
`setIntegral_ge_of_const_le_real` 📖	mathematical	`MeasurableSet` `Real` `Real.instLE` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real` `Real.instLE` `Real.instMul` `Measure.real` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`mul_comm` `setIntegral_ge_of_const_le` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instCompleteSpace`
`setIntegral_gt_gt` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `setOf` `Real.instLT`	`Real` `Real.instLT` `Real.instMul` `Measure.real` `setOf` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`aestronglyMeasurable_const` `lt_of_le_of_lt` `setLIntegral_mono_ae` `AEStronglyMeasurable.enorm` `ae_of_all` `Measure.instOuterMeasureClass` `LE.le.trans` `le_of_lt` `Real.nnnorm_of_nonneg` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Real.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `smul_eq_mul` `setIntegral_const` `Real.instCompleteSpace` `integral_sub` `setIntegral_pos_iff_support_of_nonneg_ae` `Pi.zero_def` `Filter.EventuallyLE.eq_1` `ae_restrict_iff₀` `nullMeasurableSet_le` `BorelSpace.opensMeasurable` `Real.borelSpace` `instSecondCountableTopologyReal` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `aemeasurable_zero` `AEMeasurable.sub` `ContinuousSub.measurableSub₂` `IsTopologicalAddGroup.to_continuousSub` `instIsTopologicalAddGroupReal` `AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `aemeasurable_const` `Filter.Eventually.of_forall` `sub_nonneg` `Integrable.sub` `Set.inter_eq_self_of_subset_right` `ne_of_lt` `pos_iff_ne_zero` `ENNReal.instCanonicallyOrderedAdd`
`setIntegral_indicator` 📖	mathematical	`MeasurableSet`	`integral` `Measure.restrict` `Set.indicator` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Set` `Set.instInter`	—	`integral_indicator` `Measure.restrict_restrict` `Set.inter_comm`
`setIntegral_indicatorConstLp` 📖	mathematical	`MeasurableSet`	`integral` `Measure.restrict` `AEEqFun.cast` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `AEEqFun` `AddSubgroup` `AEEqFun.instAddGroup` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `SetLike.instMembership` `AddSubgroup.instSetLike` `Lp` `indicatorConstLp` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Measure.real` `Set` `Set.instInter`	—	`setIntegral_congr_ae` `Filter.Eventually.mono` `Measure.instOuterMeasureClass` `indicatorConstLp_coeFn` `integral_indicator_const` `measureReal_restrict_apply`
`setIntegral_le_integral` 📖	mathematical	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_mono_measure` `Measure.restrict_le_self`
`setIntegral_le_nonneg` 📖	mathematical	`MeasurableSet` `StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `setOf` `Real.instZero`	—	`integral_indicator` `StronglyMeasurable.measurableSet_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace` `stronglyMeasurable_const` `integral_mono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `Integrable.indicator` `Set.indicator_le_indicator_nonneg`
`setIntegral_map` 📖	mathematical	`MeasurableSet` `AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Measure.map` `AEMeasurable`	`integral` `Measure.restrict` `Measure.map` `Set.preimage`	—	`Measure.restrict_map_of_aemeasurable` `integral_map` `AEMeasurable.mono_measure` `Measure.restrict_le_self` `AEStronglyMeasurable.mono_measure` `Measure.map_mono_of_aemeasurable`
`setIntegral_map_equiv` 📖	mathematical	—	`integral` `Measure.restrict` `Measure.map` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `Set.preimage`	—	`MeasurableEmbedding.setIntegral_map` `MeasurableEquiv.measurableEmbedding`
`setIntegral_mono` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Pi.hasLe` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`integral_mono`
`setIntegral_mono_ae` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_mono_ae_restrict` `ae_restrict_of_ae`
`setIntegral_mono_ae_restrict` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_mono_ae` `integral_def` `instReflLe`
`setIntegral_mono_on` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasurableSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`setIntegral_mono_ae_restrict` `Measure.instOuterMeasureClass` `ae_restrict_eq` `ae_of_all`
`setIntegral_mono_on_ae` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_mono_ae_restrict` `Filter.EventuallyLE.eq_1` `ae_restrict_iff'`
`setIntegral_mono_on_ae₀` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NullMeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_congr_set` `Filter.EventuallyEq.symm` `NullMeasurableSet.toMeasurable_ae_eq` `setIntegral_mono_on_ae` `integrableOn_congr_set_ae` `measurableSet_toMeasurable` `Filter.mp_mem` `Filter.EventuallyEq.mem_iff` `Filter.univ_mem'`
`setIntegral_mono_on₀` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NullMeasurableSet` `Preorder.toLE` `PartialOrder.toPreorder`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`setIntegral_mono_on_ae₀` `Filter.Eventually.of_forall` `Measure.instOuterMeasureClass`
`setIntegral_mono_set` 📖	mathematical	`IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Filter.EventuallyLE` `Preorder.toLE` `PartialOrder.toPreorder` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Prop.le`	`Preorder.toLE` `PartialOrder.toPreorder` `integral` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_mono_measure` `Measure.restrict_mono_ae`
`setIntegral_neg_eq_setIntegral_nonpos` 📖	mathematical	`AEStronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`integral` `Measure.restrict` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `Preorder.toLE`	—	`AEStronglyMeasurable.nullMeasurableSet_eq_fun` `EMetricSpace.metrizableSpace` `aestronglyMeasurable_zero` `integral_union_eq_left_of_ae` `Filter.mp_mem` `Measure.instOuterMeasureClass` `ae_restrict_mem₀` `Filter.univ_mem'`
`setIntegral_nonneg` 📖	mathematical	`MeasurableSet` `Real` `Real.instLE` `Real.instZero`	`Real` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`setIntegral_nonneg_of_ae_restrict` `Measure.instOuterMeasureClass` `ae_restrict_iff'` `ae_of_all`
`setIntegral_nonneg_ae` 📖	mathematical	`MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Real` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_nonneg_of_ae_restrict` `Filter.EventuallyLE.eq_1` `ae_restrict_iff'`
`setIntegral_nonneg_of_ae` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `Real.instZero`	`Real` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `setIntegral_nonneg_of_ae_restrict` `ae_restrict_of_ae`
`setIntegral_nonneg_of_ae_restrict` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `Real.instZero`	`Real` `Real.instLE` `Real.instZero` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict`	—	`Measure.instOuterMeasureClass` `integral_nonneg_of_ae` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal`
`setIntegral_nonpos` 📖	mathematical	`MeasurableSet` `Real` `Real.instLE` `Real.instZero`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instZero`	—	`setIntegral_nonpos_ae` `ae_of_all` `Measure.instOuterMeasureClass`
`setIntegral_nonpos_ae` 📖	mathematical	`MeasurableSet` `Filter.Eventually` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instZero`	—	`Measure.instOuterMeasureClass` `setIntegral_nonpos_of_ae_restrict` `Filter.EventuallyLE.eq_1` `ae_restrict_iff'`
`setIntegral_nonpos_le` 📖	mathematical	`MeasurableSet` `StronglyMeasurable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Integrable` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `setOf` `Real.instZero`	—	`integral_indicator` `StronglyMeasurable.measurableSet_le` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `PseudoEMetricSpace.pseudoMetrizableSpace` `stronglyMeasurable_const` `integral_mono` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `Integrable.indicator` `Set.indicator_nonpos_le_indicator`
`setIntegral_nonpos_of_ae` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Pi.instZero` `Real.instZero`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instZero`	—	`Measure.instOuterMeasureClass` `setIntegral_nonpos_of_ae_restrict` `ae_restrict_of_ae`
`setIntegral_nonpos_of_ae_restrict` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `Real.instZero`	`Real` `Real.instLE` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instZero`	—	`Measure.instOuterMeasureClass` `integral_nonpos_of_ae` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal`
`setIntegral_one_eq_measureReal` 📖	mathematical	—	`integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `Real.instOne` `Measure.real`	—	`integral_const` `Real.instCompleteSpace` `measureReal_restrict_apply` `Set.univ_inter` `mul_one`
`setIntegral_pos_iff_support_of_nonneg_ae` 📖	mathematical	`Filter.EventuallyLE` `Real` `Real.instLE` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.restrict` `Pi.instZero` `Real.instZero` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`Real` `Real.instLT` `Real.instZero` `integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `Measure.restrict` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `DFunLike.coe` `Measure` `Set` `Measure.instFunLike` `Set.instInter` `Function.support`	—	`Measure.instOuterMeasureClass` `integral_pos_iff_support_of_nonneg_ae` `Measure.restrict_apply₀` `Function.support_eq_preimage` `AEMeasurable.nullMeasurable` `AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Real.borelSpace` `Integrable.aestronglyMeasurable` `MeasurableSet.compl` `MeasurableSingletonClass.measurableSet_singleton` `instMeasurableSingletonClassOfMeasurableEq` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `instSecondCountableTopologyReal` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace`
`setIntegral_support` 📖	mathematical	—	`integral` `Measure.restrict` `Function.support` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`setIntegral_univ` `setIntegral_eq_of_subset_of_forall_diff_eq_zero` `MeasurableSet.univ` `Set.subset_univ` `Function.notMem_support` `Set.notMem_of_mem_diff`
`setIntegral_trim` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `StronglyMeasurable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasurableSet`	`integral` `Measure.restrict` `Measure.trim`	—	`integral_trim` `restrict_trim`
`setIntegral_tsupport` 📖	mathematical	—	`integral` `Measure.restrict` `tsupport` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	—	`setIntegral_univ` `setIntegral_eq_of_subset_of_forall_diff_eq_zero` `MeasurableSet.univ` `Set.subset_univ` `image_eq_zero_of_notMem_tsupport` `Set.notMem_of_mem_diff`
`setIntegral_union` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `MeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set` `Set.instUnion` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`setIntegral_union₀` `Disjoint.aedisjoint` `MeasurableSet.nullMeasurableSet`
`setIntegral_union₀` 📖	mathematical	`AEDisjoint` `NullMeasurableSet` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`integral` `Measure.restrict` `Set` `Set.instUnion` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid`	—	`Measure.restrict_union₀` `integral_add_measure`
`setIntegral_univ` 📖	mathematical	—	`integral` `Measure.restrict` `Set.univ`	—	`Measure.restrict_univ`
`tendsto_setIntegral_of_antitone` 📖	mathematical	`MeasurableSet` `Antitone` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`Filter.Tendsto` `integral` `Measure.restrict` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.iInter`	—	`Filter.Tendsto.of_neBot_imp` `Filter.atTop_neBot_iff` `Filter.Tendsto.sub` `IsTopologicalAddGroup.to_continuousSub` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `tendsto_const_nhds` `tendsto_setIntegral_of_monotone` `Set.diff_subset_diff_right` `Set.diff_iInter` `IntegrableOn.mono_set` `Set.diff_subset` `setIntegral_diff` `MeasurableSet.iInter_of_antitone` `Set.iInter_subset` `sub_sub_cancel` `Filter.Tendsto.congr'` `Filter.Eventually.mono` `Filter.eventually_ge_atTop`
`tendsto_setIntegral_of_monotone` 📖	mathematical	`MeasurableSet` `Monotone` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`Filter.Tendsto` `integral` `Measure.restrict` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.iUnion`	—	`tendsto_setIntegral_of_monotone₀` `MeasurableSet.nullMeasurableSet`
`tendsto_setIntegral_of_monotone₀` 📖	mathematical	`NullMeasurableSet` `Monotone` `Set` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `IntegrableOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Set.iUnion`	`Filter.Tendsto` `integral` `Measure.restrict` `Filter.atTop` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `Set.iUnion`	—	`Filter.Tendsto.of_neBot_imp` `Filter.atTop_neBot_iff` `MeasurableSet.iUnion_of_monotone` `Set.subset_iUnion` `Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_closedBall` `CanLift.prf` `NNReal.canLift` `LT.lt.le` `tendsto_measure_iUnion_atTop` `ENNReal.Icc_mem_nhds` `LT.lt.ne` `withDensity_apply₀` `LT.lt.ne'` `ENNReal.coe_pos` `Filter.mp_mem` `Filter.univ_mem'` `mem_closedBall_iff_norm'` `setIntegral_diff₀` `coe_nnnorm` `NNReal.coe_le_coe` `ENNReal.coe_le_coe` `LE.le.trans` `enorm_integral_le_lintegral_enorm` `NullMeasurableSet.mono_ac` `withDensity_absolutelyContinuous` `NullMeasurableSet.diff` `measure_diff` `LE.le.trans_lt` `ENNReal.add_lt_top` `ENNReal.coe_lt_top` `tsub_le_iff_tsub_le` `ENNReal.instOrderedSub`

MeasureTheory.Integrable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`measure_le_integral` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Filter.EventuallyLE` `Real.instLE` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `Pi.instZero` `Real.instZero` `Real.instOne`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `ENNReal.ofReal` `MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ofReal_integral_eq_lintegral_ofReal` `MeasureTheory.meas_le_lintegral₀` `Measurable.comp_aemeasurable` `Continuous.measurable` `BorelSpace.opensMeasurable` `Real.borelSpace` `ENNReal.borelSpace` `ENNReal.continuous_ofReal` `MeasureTheory.AEStronglyMeasurable.aemeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `ENNReal.ofReal_one` `ENNReal.ofReal_le_ofReal`
`simpleFunc_mul` 📖	mathematical	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Pi.instMul` `Real.instMul` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike`	—	`MeasureTheory.SimpleFunc.induction` `Set.piecewise_eq_indicator` `Set.indicator_of_mem` `Set.indicator_of_notMem` `MulZeroClass.zero_mul` `MeasureTheory.integrable_indicator_iff` `integrableOn` `smul` `Real.isBoundedSMul` `congr` `add` `IsSemitopologicalSemiring.toContinuousAdd` `IsSemitopologicalRing.toIsSemitopologicalSemiring` `IsTopologicalRing.toIsSemitopologicalRing` `instIsTopologicalRingReal` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.SimpleFunc.coe_add` `add_mul` `Distrib.rightDistribClass` `Filter.EventuallyEq.refl`
`simpleFunc_mul'` 📖	mathematical	`MeasurableSpace` `MeasurableSpace.instLE` `MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing`	`MeasureTheory.Integrable` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `Pi.instMul` `Real.instMul` `DFunLike.coe` `MeasureTheory.SimpleFunc` `MeasureTheory.SimpleFunc.instFunLike`	—	`MeasureTheory.SimpleFunc.coe_toLargerSpace_eq` `simpleFunc_mul`

MeasureTheory.MeasurePreserving

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`setIntegral_image_emb` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Set.image`	—	`integral_comp` `restrict_image_emb`
`setIntegral_preimage_emb` 📖	mathematical	`MeasureTheory.MeasurePreserving` `MeasurableEmbedding`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `Set.preimage`	—	`integral_comp` `restrict_preimage_emb`

Topology.IsClosedEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`setIntegral_map` 📖	mathematical	`Topology.IsClosedEmbedding`	`MeasureTheory.integral` `MeasureTheory.Measure.restrict` `MeasureTheory.Measure.map` `Set.preimage`	—	`MeasurableEmbedding.setIntegral_map` `measurableEmbedding`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuousOn_integral_bilinear_of_locally_integrable_of_compact_support` 📖	mathematical	`IsCompact` `ContinuousOn` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup` `MeasureTheory.IntegrableOn` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.integral` `DFunLike.coe` `ContinuousLinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `RingHom.id` `Semiring.toNonAssocSemiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `ContinuousLinearMap.funLike` `ContinuousLinearMap.topologicalSpace` `NormedAddCommGroup.toAddCommGroup` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContinuousLinearMap.addCommMonoid` `IsTopologicalAddGroup.toContinuousAdd` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `ContinuousLinearMap.module` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `UniformContinuousConstSMul.to_continuousConstSMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsBoundedSMul.toUniformContinuousConstSMul` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedSpace.toIsBoundedSMul`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `ContinuousOn.comp_continuous` `Continuous.prodMk_right` `Metric.continuousWithinAt_iff'` `RingHomIsometric.ids` `MeasureTheory.integral_mul_const` `exists_pos_mul_lt` `Real.instIsStrictOrderedRing` `IsCompact.mem_uniformity_of_prod` `ContinuousOn.mono` `Set.prod_mono_right` `Set.subset_univ` `Metric.dist_mem_uniformity` `dist_eq_norm` `ContinuousOn.prodMk` `continuousOn_const` `continuousOn_id'` `ContinuousOn.comp` `IsCompact.exists_bound_of_continuousOn` `LE.le.trans` `le_max_left` `norm_zero` `MeasureTheory.Integrable.mul_const` `MeasureTheory.Integrable.const_mul` `MeasureTheory.Integrable.norm` `MeasureTheory.Integrable.mono'` `ContinuousLinearMap.aestronglyMeasurable_comp₂` `MeasureTheory.Integrable.aestronglyMeasurable` `MeasureTheory.StronglyMeasurable.aestronglyMeasurable` `Continuous.stronglyMeasurable_of_support_subset_isCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Function.support_subset_iff'` `Filter.Eventually.of_forall` `MeasureTheory.Measure.instOuterMeasureClass` `ContinuousLinearMap.le_opNorm₂` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `mul_nonneg` `norm_nonneg` `Filter.mp_mem` `self_mem_nhdsWithin` `Filter.univ_mem'` `MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `ContinuousSemilinearMapClass.toSemilinearMapClass` `ContinuousLinearMap.continuousSemilinearMapClass` `MeasureTheory.integral_sub` `MeasureTheory.norm_integral_le_integral_norm` `MeasureTheory.integral_mono_of_nonneg` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `map_sub` `le_of_lt` `sub_self`
`continuousOn_integral_of_compact_support` 📖	mathematical	`IsCompact` `ContinuousOn` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SProd.sprod` `Set` `Set.instSProd` `Set.univ` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `NormedAddCommGroup.toAddCommGroup`	`ContinuousOn` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.integral`	—	`SeminormedAddCommGroup.toIsTopologicalAddGroup` `IsTopologicalAddGroup.toContinuousAdd` `smulCommClass_self` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `IsScalarTower.left` `one_smul` `continuousOn_integral_bilinear_of_locally_integrable_of_compact_support` `MeasureTheory.integrableOn_const` `IsCompact.measure_ne_top` `enorm_ne_top`
`continuous_parametric_integral_of_continuous` 📖	mathematical	`Continuous` `instTopologicalSpaceProd` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `IsCompact`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `MeasureTheory.integral` `MeasureTheory.Measure.restrict`	—	`continuous_iff_continuousAt` `WeaklyLocallyCompactSpace.exists_compact_mem_nhds` `instWeaklyLocallyCompactSpaceOfLocallyCompactSpace` `IsCompact.bddAbove_image` `instClosedIciTopology` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `Real.instIsOrderedAddMonoid` `IsCompact.prod` `Continuous.continuousOn` `Continuous.norm` `MeasureTheory.continuousAt_of_dominated` `Filter.univ_mem'` `Continuous.aestronglyMeasurable` `PseudoEMetricSpace.pseudoMetrizableSpace` `Continuous.comp'` `Continuous.prodMk` `continuous_const` `continuous_id'` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.ae_restrict_iff` `IsClosed.measurableSet` `isClosed_le` `Set.mem_image_of_mem` `Set.mk_mem_prod` `MeasureTheory.integrableOn_const` `IsCompact.measure_ne_top` `isFiniteMeasureOnCompacts_of_isLocallyFiniteMeasure` `enorm_ne_top` `Continuous.continuousAt`
`measure_le_lintegral_thickenedIndicator` 📖	mathematical	`MeasurableSet` `Real` `Real.instLT` `Real.instZero`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.lintegral` `ENNReal.ofNNReal` `BoundedContinuousFunction` `NNReal` `UniformSpace.toTopologicalSpace` `PseudoEMetricSpace.toUniformSpace` `instPseudoMetricSpaceNNReal` `BoundedContinuousFunction.instFunLike` `thickenedIndicator`	—	`ENNReal.coe_toNNReal` `LT.lt.ne` `thickenedIndicatorAux_lt_top` `measure_le_lintegral_thickenedIndicatorAux`
`measure_le_lintegral_thickenedIndicatorAux` 📖	mathematical	`MeasurableSet`	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `DFunLike.coe` `MeasureTheory.Measure` `Set` `MeasureTheory.Measure.instFunLike` `MeasureTheory.lintegral` `thickenedIndicatorAux`	—	`MeasureTheory.lintegral_indicator` `MeasureTheory.lintegral_one` `MeasureTheory.Measure.restrict_apply` `Set.univ_inter` `MeasureTheory.lintegral_mono` `indicator_le_thickenedIndicatorAux`

---

← Back to Index