Sub

📁 Source: Mathlib/MeasureTheory/Integral/Lebesgue/Sub.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_measurable_le_setLIntegral_eq_of_integrable, exists_setLIntegral_compl_lt, lintegral_iInf, lintegral_iInf', lintegral_iInf_ae, lintegral_iInf_directed_of_measurable, lintegral_sub, lintegral_sub', lintegral_sub_le, lintegral_sub_le', lintegral_tendsto_of_tendsto_of_antitone	11
Total	11

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_measurable_le_setLIntegral_eq_of_integrable 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder lintegral Measure.restrict	—	exists_measurable_le_lintegral_eq le_antisymm compl_compl setLIntegral_compl MeasurableSet.compl ne_top_of_le_ne_top setLIntegral_le_lintegral tsub_le_tsub ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid le_refl lintegral_mono_fn' lintegral_mono
exists_setLIntegral_compl_lt 📖	mathematical	—	MeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Top.top instTopENNReal lintegral Measure.restrict Compl.compl Set.instCompl	—	MeasurableSet.empty measure_empty Measure.instOuterMeasureClass Set.compl_empty Measure.restrict_univ ENNReal.instCanonicallyOrderedAdd ENNReal.sub_lt_self SimpleFunc.measurable SimpleFunc.FinMeasSupp.of_lintegral_ne_top ne_top_of_le_ne_top lintegral_mono SimpleFunc.lintegral_eq_lintegral measurableSet_support instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space setLIntegral_congr_fun MeasurableSet.compl tsub_zero ENNReal.instOrderedSub setLIntegral_le_lintegral lintegral_sub ae_of_all ENNReal.sub_lt_of_lt_add ENNReal.lt_add_of_sub_lt_left
lintegral_iInf 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Antitone Nat.instPreorder Pi.preorder PartialOrder.toPreorder ENNReal.instPartialOrder	lintegral iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	lintegral_iInf_ae ae_of_all Measure.instOuterMeasureClass
lintegral_iInf' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Antitone Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Measure.instOuterMeasureClass aeSeq.prop_of_mem_aeSeqSet le_rfl lintegral_congr_ae Filter.EventuallyEq.symm aeSeq.iInf instCountableNat iInf_apply lintegral_iInf aeSeq.measurable aeSeq.aeSeq_n_eq_fun_n_ae
lintegral_iInf_ae 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Measure.instOuterMeasureClass lintegral_mono iInf_le_of_le le_rfl lintegral_sub Measurable.iInf ENNReal.borelSpace ENNReal.instOrderTopology ENNReal.instSecondCountableTopology instCountableNat ne_top_of_le_ne_top iInf_le ae_of_all ENNReal.sub_iInf lintegral_iSup_ae Measurable.sub ENNReal.instMeasurableSub₂ Filter.Eventually.mono tsub_le_tsub ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid ae_all_iff le_refl LE.le.trans lintegral_mono_ae
lintegral_iInf_directed_of_measurable 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Directed Pi.hasLe Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	lintegral iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	nonempty_encodable isEmpty_or_nonempty iInf_of_empty lintegral_const ENNReal.top_mul Measure.measure_univ_ne_zero le_antisymm le_iInf iInf_le iInf_le_of_le Directed.sequence_le lintegral_iInf Directed.sequence_anti lintegral_mono
lintegral_sub 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral ENNReal.instSub	—	Measure.instOuterMeasureClass lintegral_sub' Measurable.aemeasurable
lintegral_sub' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass	lintegral ENNReal.instSub	—	Measure.instOuterMeasureClass ENNReal.eq_sub_of_add_eq lintegral_add_right' lintegral_congr_ae Filter.Eventually.mono tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE ENNReal.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid ENNReal.instOrderedSub
lintegral_sub_le 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub lintegral	—	lintegral_sub_le' Measurable.aemeasurable
lintegral_sub_le' 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace	Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub lintegral	—	tsub_le_iff_right ENNReal.instOrderedSub add_top le_top lintegral_add_right' lintegral_mono_fn' le_refl le_tsub_add
lintegral_tendsto_of_tendsto_of_antitone 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Filter.Eventually Antitone Nat.instPreorder PartialOrder.toPreorder ENNReal.instPartialOrder ae Measure Measure.instFunLike Measure.instOuterMeasureClass Filter.Tendsto Filter.atTop nhds ENNReal.instTopologicalSpace	lintegral	—	Measure.instOuterMeasureClass lintegral_mono_ae Filter.Eventually.mono lintegral_iInf' lintegral_congr_ae Filter.mp_mem Filter.univ_mem' tendsto_nhds_unique ENNReal.instT2Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_atTop_iInf LinearOrder.infConvergenceClass ENNReal.instOrderTopology

---

← Back to Index