MeasureSpace

📁 Source: Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Statistics

Metric	Count
Definitions coeAddHom, cofinite, instAdd, instAddCommMonoid, instCompleteLattice, instCompleteSemilatticeInf, instDistribMulAction, instInfSet, instInhabited, instModule, instMulAction, instPartialOrder, instSMul, instZero, sum, MeasureSpace, toMeasure	17
Theorems nullMeasurable, nullMeasurableSet_preimage, measure_iInter, measure_iUnion, measure_iInter, measure_iUnion, Ico_ae_eq_Icc', Ico_ae_eq_Ioc', Iio_ae_eq_Iic', Ioc_ae_eq_Icc', Ioi_ae_eq_Ici', Ioo_ae_eq_Icc', Ioo_ae_eq_Ico', Ioo_ae_eq_Ioc', add_apply, add_toOuterMeasure, add_top, neBot, ae_ennreal_smul_measure_eq, ae_ennreal_smul_measure_iff, ae_smul_measure, ae_smul_measure_eq, ae_smul_measure_iff, ae_smul_measure_le, ae_sum_eq, ae_sum_iff, ae_sum_iff', apply_eq_zero_of_isEmpty, coeAddHom_apply, coe_add, coe_finset_sum, coe_nnreal_smul_apply, coe_smul, coe_zero, instIsMeasurablyGenerated, cofinite_le_ae, compl_mem_cofinite, ennreal_smul_eq_zero, eq_zero_of_isEmpty, eventually_cofinite, finset_sum_apply, inf_apply, instIsCentralScalar, instIsOrderedAddMonoid, instIsScalarTower, instModuleIsTorsionFree, instNeZeroENNRealCoeSetUniv, instSMulCommClass, instSubsingleton, le_add_left, le_add_right, le_iff, le_iff', le_intro, le_sum, le_sum_apply, lt_iff, lt_iff', measure_eq_left_of_subset_of_measure_add_eq, measure_eq_right_of_subset_of_measure_add_eq, measure_inter_eq_of_ae, measure_inter_eq_of_measure_eq, measure_mono_both, measure_mono_left, measure_support_eq_zero_iff, measure_toMeasurable_add_inter_left, measure_toMeasurable_add_inter_right, measure_toMeasurable_inter, measure_univ_eq_zero, measure_univ_ne_zero, measure_univ_pos, mem_cofinite, nnreal_smul_coe_apply, nonempty_of_neZero, nonpos_iff_eq_zero', sInf_apply, sInf_caratheodory, smul_apply, smul_toOuterMeasure, sum_add_sum, sum_add_sum_compl, sum_apply, sum_apply_eq_zero, sum_apply_eq_zero', sum_apply_of_countable, sum_apply₀, sum_bool, sum_coe_finset, sum_comm, sum_comp_equiv, sum_cond, sum_congr, sum_eq_zero, sum_extend_zero, sum_fintype, sum_of_isEmpty, sum_sum, sum_zero, toOuterMeasure_le, toOuterMeasure_top, top_add, zero_le, zero_toOuterMeasure, toMeasure_eq_zero, toMeasure_top, toMeasure_zero, ae_eq_bot, ae_eq_of_ae_subset_of_measure_ge, ae_eq_of_subset_of_measure_ge, ae_isMeasurablyGenerated, ae_neBot, ae_uIoc_iff, ae_zero, biSup_measure_Iic, boundedBy_measure, exists_measure_iInter_lt, exists_nonempty_inter_of_measure_univ_lt_sum_measure, exists_nonempty_inter_of_measure_univ_lt_tsum_measure, ext_of_measurableAtoms, le_measure_diff, le_measure_symmDiff, le_toMeasure_apply, le_toOuterMeasure_caratheodory, measure_add_diff, measure_add_measure_compl, measure_biUnion, measure_biUnion_eq_iSup, measure_biUnion_finset, measure_biUnion_finset₀, measure_biUnion_toMeasurable, measure_biUnion₀, measure_compl, measure_compl₀, measure_diff, measure_diff', measure_diff_add_inter, measure_diff_eq_top, measure_diff_le_iff_le_add, measure_diff_lt_of_lt_add, measure_diff_null', measure_eq_measure_larger_of_between_null_diff, measure_eq_measure_of_between_null_diff, measure_eq_measure_of_null_diff, measure_eq_measure_smaller_of_between_null_diff, measure_eq_top_iff_of_symmDiff, measure_iInter_eq_iInf_measure_iInter_le, measure_iUnion_congr_of_subset, measure_iUnion_eq_iSup_accumulate, measure_iUnion_toMeasurable, measure_if, measure_inter_add_diff, measure_inter_conull, measure_inter_conull', measure_ne_top_iff_of_symmDiff, measure_preimage_eq_zero_iff_of_countable, measure_sUnion, measure_sUnion₀, measure_symmDiff_eq, measure_symmDiff_eq_top, measure_symmDiff_le, measure_toMeasurable_union, measure_union, measure_union', measure_union_add_inter, measure_union_add_inter', measure_union_congr_of_subset, measure_union_toMeasurable, nonempty_inter_of_measure_lt_add, nonempty_inter_of_measure_lt_add', sum_measure_le_measure_univ, sum_measure_preimage_singleton, sum_measure_singleton, tendsto_measure_Ici_atBot, tendsto_measure_Ico_atTop, tendsto_measure_Iic_atTop, tendsto_measure_Ioc_atBot, tendsto_measure_biInter_gt, tendsto_measure_iInter_atBot, tendsto_measure_iInter_atTop, tendsto_measure_iInter_le, tendsto_measure_iUnion_accumulate, tendsto_measure_iUnion_atBot, tendsto_measure_iUnion_atTop, toMeasure_apply, toMeasure_apply₀, toMeasure_toOuterMeasure, toOuterMeasure_toMeasure, tsum_meas_le_meas_iUnion_of_disjoint, tsum_meas_le_meas_iUnion_of_disjoint₀, tsum_measure_le_measure_univ, tsum_measure_preimage_singleton, union_ae_eq_left_iff_ae_subset, union_ae_eq_right_iff_ae_subset, measure_iInter, measure_iUnion	195
Total	212

AEMeasurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nullMeasurable 📖	mathematical	AEMeasurable	MeasureTheory.NullMeasurable	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.NullMeasurable.congr Measurable.nullMeasurable Filter.EventuallyEq.symm
nullMeasurableSet_preimage 📖	mathematical	AEMeasurable MeasurableSet	MeasureTheory.NullMeasurableSet Set.preimage	—	nullMeasurable

Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_iInter 📖	mathematical	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MeasureTheory.NullMeasurableSet	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Monotone.measure_iInter OrderDual.isDirected_ge OrderDual.instIsCountablyGeneratedAtBot dual_left
measure_iUnion 📖	mathematical	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Monotone.measure_iUnion OrderDual.isDirected_le OrderDual.instIsCountablyGeneratedAtTop dual_left

Directed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_iInter 📖	mathematical	MeasureTheory.NullMeasurableSet Directed Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	ne_top_of_le_ne_top MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass ENNReal.sub_sub_cancel iInf_le ENNReal.sub_iInf Set.iInter_subset MeasureTheory.measure_diff MeasureTheory.NullMeasurableSet.iInter Set.diff_iInter measure_iUnion mono_comp Set.diff_subset_diff_right le_antisymm iSup_mono' Set.diff_subset_diff subset_refl Set.instReflSubset iSup_mono MeasureTheory.le_measure_diff
measure_iUnion 📖	mathematical	Directed Set Set.instHasSubset	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Countable.exists_injective_nat extend_bot le_antisymm MeasurableSet.disjointed MeasureTheory.measurableSet_toMeasurable iUnion_disjointed MeasureTheory.measure_iUnion_toMeasurable instCountableNat MeasureTheory.measure_iUnion_le MeasureTheory.Measure.instOuterMeasureClass ENNReal.tsum_eq_iSup_sum iSup_le finset_le Set.instIsTransSubset MeasureTheory.measure_biUnion_finset Pairwise.set_pairwise disjoint_disjointed MeasureTheory.measure_mono Set.iUnion₂_mono disjointed_subset MeasureTheory.measure_biUnion_toMeasurable Finset.countable_toSet Set.iUnion₂_subset le_iSup Set.subset_iUnion iSup_extend_bot Function.apply_extend MeasureTheory.measure_empty

MeasureTheory

Definitions

Name	Category	Theorems
MeasureSpace 📖	CompData	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Ico_ae_eq_Icc' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ico PartialOrder.toPreorder Set.Icc	—	Filter.EventuallyEq.inter Measure.instOuterMeasureClass ae_eq_refl Iio_ae_eq_Iic'
Ico_ae_eq_Ioc' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ico PartialOrder.toPreorder Set.Ioc	—	Filter.EventuallyEq.trans Measure.instOuterMeasureClass Filter.EventuallyEq.symm Ioo_ae_eq_Ico' Ioo_ae_eq_Ioc'
Iio_ae_eq_Iic' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Iio PartialOrder.toPreorder Set.Iic	—	Measure.instOuterMeasureClass Set.Iic_diff_right diff_ae_eq_self measure_mono_null Set.inter_subset_right
Ioc_ae_eq_Icc' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ioc PartialOrder.toPreorder Set.Icc	—	Filter.EventuallyEq.inter Measure.instOuterMeasureClass Ioi_ae_eq_Ici' ae_eq_refl
Ioi_ae_eq_Ici' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ioi PartialOrder.toPreorder Set.Ici	—	Iio_ae_eq_Iic'
Ioo_ae_eq_Icc' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ioo PartialOrder.toPreorder Set.Icc	—	Filter.EventuallyEq.inter Measure.instOuterMeasureClass Ioi_ae_eq_Ici' Iio_ae_eq_Iic'
Ioo_ae_eq_Ico' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ioo PartialOrder.toPreorder Set.Ico	—	Filter.EventuallyEq.inter Measure.instOuterMeasureClass Ioi_ae_eq_Ici' ae_eq_refl
Ioo_ae_eq_Ioc' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSingletonSet instZeroENNReal	Filter.EventuallyEq ae Measure.instOuterMeasureClass Set.Ioo PartialOrder.toPreorder Set.Ioc	—	Filter.EventuallyEq.inter Measure.instOuterMeasureClass ae_eq_refl Iio_ae_eq_Iic'
ae_eq_bot 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Bot.bot Filter Filter.instBot Measure.instZero	—	Measure.instOuterMeasureClass Filter.empty_mem_iff_bot mem_ae_iff Set.compl_empty Measure.measure_univ_eq_zero
ae_eq_of_ae_subset_of_measure_ge 📖	mathematical	Filter.EventuallyLE Prop.le ae Measure Measure.instFunLike Measure.instOuterMeasureClass ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Set NullMeasurableSet	Filter.EventuallyEq	—	Measure.instOuterMeasureClass Filter.eventuallyLE_antisymm_iff ae_le_set LE.le.antisymm measure_mono_ae measure_diff' measure_congr union_ae_eq_left_iff_ae_subset tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
ae_eq_of_subset_of_measure_ge 📖	mathematical	Set Set.instHasSubset ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike NullMeasurableSet	Filter.EventuallyEq ae Measure.instOuterMeasureClass	—	ae_eq_of_ae_subset_of_measure_ge HasSubset.Subset.eventuallyLE Measure.instOuterMeasureClass
ae_isMeasurablyGenerated 📖	mathematical	—	Filter.IsMeasurablyGenerated ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass exists_measurable_superset_of_null compl_mem_ae_iff MeasurableSet.compl Set.compl_subset_comm
ae_neBot 📖	mathematical	—	Filter.NeBot ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Filter.neBot_iff ae_eq_bot
ae_uIoc_iff 📖	mathematical	—	Filter.Eventually ae Measure Measure.instFunLike Measure.instOuterMeasureClass	—	Measure.instOuterMeasureClass Set.uIoc_eq_union
ae_zero 📖	mathematical	—	ae Measure Measure.instFunLike Measure.instOuterMeasureClass Measure.instZero Bot.bot Filter Filter.instBot	—	Measure.instOuterMeasureClass ae_eq_bot
biSup_measure_Iic 📖	mathematical	Set Set.instMembership Preorder.toLE DirectedOn	iSup ENNReal ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DFunLike.coe Measure Measure.instFunLike Set.Iic Set.univ	—	measure_biUnion_eq_iSup directedOn_iff_directed Directed.mono_comp Set.Iic_subset_Iic DirectedOn.directed_val Set.iUnion₂_eq_univ_iff
boundedBy_measure 📖	mathematical	—	OuterMeasure.boundedBy DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.toOuterMeasure	—	OuterMeasure.boundedBy_eq_self
exists_measure_iInter_lt 📖	mathematical	NullMeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal Set.iInter Set Set.instEmptyCollection	DFunLike.coe Measure Measure.instFunLike Preorder.toLE SemilatticeSup.toPartialOrder	—	measure_mono Measure.instOuterMeasureClass Set.biInter_subset_biInter_left le_trans measure_empty tendsto_measure_iInter_le ENNReal.tendsto_atTop_zero_iff_lt_of_antitone
exists_nonempty_inter_of_measure_univ_lt_sum_measure 📖	mathematical	NullMeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.univ Finset.sum ENNReal.instAddCommMonoid	Finset Finset.instMembership Set.Nonempty Set.instInter	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq sum_measure_le_measure_univ Disjoint.aedisjoint Set.disjoint_iff_inter_eq_empty
exists_nonempty_inter_of_measure_univ_lt_tsum_measure 📖	mathematical	NullMeasurableSet ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Set.univ tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	Set.Nonempty Set.instInter	—	Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq tsum_measure_le_measure_univ Disjoint.aedisjoint Set.disjoint_iff_inter_eq_empty
ext_of_measurableAtoms 📖	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike measurableAtom	—	—	Measure.ext Set.ext mem_measurableAtom_self mem_of_mem_measurableAtom Set.sUnion_image Set.Countable.image Set.to_countable SetCoe.countable disjoint_measurableAtom_of_notMem measurableAtom_eq_of_mem MeasurableSet.measurableAtom_of_countable measure_sUnion
le_measure_diff 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub DFunLike.coe Measure Set Measure.instFunLike Set.instSDiff	—	tsub_le_iff_left ENNReal.instOrderedSub LE.le.trans measure_le_inter_add_diff Measure.instOuterMeasureClass add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid measure_mono Set.inter_subset_right
le_measure_symmDiff 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub DFunLike.coe Measure Set Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	le_trans le_measure_diff measure_mono Measure.instOuterMeasureClass
le_toMeasure_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE OuterMeasure.caratheodory	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe OuterMeasure Set OuterMeasure.instFunLikeSetENNReal Measure Measure.instFunLike OuterMeasure.toMeasure	—	OuterMeasure.le_trim
le_toOuterMeasure_caratheodory 📖	mathematical	—	MeasurableSpace MeasurableSpace.instLE OuterMeasure.caratheodory Measure.toOuterMeasure	—	measure_inter_add_diff
measure_add_diff 📖	mathematical	NullMeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instSDiff Set.instUnion	—	measure_union₀' Disjoint.aedisjoint Set.disjoint_sdiff_right Set.union_diff_self
measure_add_measure_compl 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Compl.compl Set.instCompl Set.univ	—	measure_add_measure_compl₀ MeasurableSet.nullMeasurableSet
measure_biUnion 📖	mathematical	Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.iUnion Set.instMembership tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	measure_biUnion₀ Set.PairwiseDisjoint.aedisjoint MeasurableSet.nullMeasurableSet
measure_biUnion_eq_iSup 📖	mathematical	DirectedOn Function.onFun Set Set.instHasSubset	DFunLike.coe Measure ENNReal Measure.instFunLike Set.iUnion Set.instMembership iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	Set.biUnion_eq_iUnion Directed.measure_iUnion Set.Countable.to_subtype DirectedOn.directed_val iSup_subtype''
measure_biUnion_finset 📖	mathematical	Set.PairwiseDisjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset Finset.instSetLike MeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.iUnion Finset.instMembership Finset.sum ENNReal.instAddCommMonoid	—	measure_biUnion_finset₀ Set.PairwiseDisjoint.aedisjoint MeasurableSet.nullMeasurableSet
measure_biUnion_finset₀ 📖	mathematical	Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Set AEDisjoint NullMeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.iUnion Finset.instMembership Finset.sum ENNReal.instAddCommMonoid	—	Finset.sum_attach Finset.attach_eq_univ tsum_fintype SummationFilter.instLeAtTopUnconditional measure_biUnion₀ Finset.countable_toSet
measure_biUnion_toMeasurable 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.iUnion Set.instMembership toMeasurable	—	Set.biUnion_eq_iUnion measure_iUnion_toMeasurable Encodable.countable
measure_biUnion₀ 📖	mathematical	Set.Pairwise Function.onFun Set AEDisjoint NullMeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.iUnion Set.instMembership tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	Set.biUnion_eq_iUnion measure_iUnion₀ Encodable.countable Set.Pairwise.on_injective Subtype.coe_injective
measure_compl 📖	mathematical	MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl ENNReal.instSub Set.univ	—	measure_compl₀ MeasurableSet.nullMeasurableSet
measure_compl₀ 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl ENNReal.instSub Set.univ	—	measure_add_measure_compl₀ ENNReal.add_sub_cancel_left
measure_diff 📖	mathematical	Set Set.instHasSubset NullMeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.instSDiff ENNReal.instSub	—	measure_diff' Set.union_eq_self_of_subset_right
measure_diff' 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff ENNReal.instSub Set.instUnion	—	ENNReal.eq_sub_of_add_eq add_comm measure_add_diff Set.union_comm
measure_diff_add_inter 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instSDiff Set.instInter	—	add_comm measure_inter_add_diff
measure_diff_eq_top 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Top.top instTopENNReal	Set.instSDiff	—	Mathlib.Tactic.Contrapose.contrapose₁ LT.lt.ne LE.le.trans_lt measure_mono Measure.instOuterMeasureClass Set.subset_diff_union measure_union_le ENNReal.add_lt_top Ne.lt_top
measure_diff_le_iff_le_add 📖	mathematical	NullMeasurableSet Set Set.instHasSubset	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike Set.instSDiff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	measure_diff tsub_le_iff_left ENNReal.instOrderedSub
measure_diff_lt_of_lt_add 📖	mathematical	NullMeasurableSet Set Set.instHasSubset ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	Set.instSDiff	—	measure_diff ENNReal.sub_lt_of_lt_add measure_mono Measure.instOuterMeasureClass add_comm
measure_diff_null' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instInter instZeroENNReal	Set.instSDiff	—	measure_congr Measure.instOuterMeasureClass diff_ae_eq_self
measure_eq_measure_larger_of_between_null_diff 📖	—	Set Set.instHasSubset DFunLike.coe Measure ENNReal Measure.instFunLike Set.instSDiff instZeroENNReal	—	—	measure_eq_measure_of_between_null_diff
measure_eq_measure_of_between_null_diff 📖	—	Set Set.instHasSubset DFunLike.coe Measure ENNReal Measure.instFunLike Set.instSDiff instZeroENNReal	—	—	measure_mono Measure.instOuterMeasureClass Set.diff_union_of_subset HasSubset.Subset.trans Set.instIsTransSubset measure_union_le zero_add LE.le.antisymm LE.le.trans
measure_eq_measure_of_null_diff 📖	—	Set Set.instHasSubset DFunLike.coe Measure ENNReal Measure.instFunLike Set.instSDiff instZeroENNReal	—	—	measure_congr Measure.instOuterMeasureClass Filter.EventuallyLE.antisymm HasSubset.Subset.eventuallyLE ae_le_set
measure_eq_measure_smaller_of_between_null_diff 📖	—	Set Set.instHasSubset DFunLike.coe Measure ENNReal Measure.instFunLike Set.instSDiff instZeroENNReal	—	—	measure_eq_measure_of_between_null_diff
measure_eq_top_iff_of_symmDiff 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Top.top instTopENNReal	—	Set.symmDiff_def eq_top_iff ENNReal.sub_eq_top_iff le_measure_diff measure_mono Measure.instOuterMeasureClass Set.subset_union_left symmDiff_comm
measure_iInter_eq_iInf_measure_iInter_le 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Preorder.toLE	—	Antitone.measure_iInter Filter.atTop.isCountablyGenerated Set.biInter_mono Set.Iic_subset_Iic Set.Subset.rfl NullMeasurableSet.biInter Set.to_countable SetCoe.countable ne_top_of_le_ne_top measure_mono Measure.instOuterMeasureClass Set.iInter₂_subset le_refl Set.iInter_comm Set.iInter_congr biInf_const Set.nonempty_Ici
measure_iUnion_congr_of_subset 📖	mathematical	Set Set.instHasSubset ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike	Set.iUnion	—	le_antisymm measure_mono Measure.instOuterMeasureClass Set.iUnion_mono'' le_top Set.subset_iUnion ae_eq_of_subset_of_measure_ge Set.inter_subset_left measure_toMeasurable Set.subset_inter HasSubset.Subset.trans Set.instIsTransSubset subset_toMeasurable Set.iUnion_mono measure_congr Filter.EventuallyEq.symm EventuallyEq.countable_iUnion instCountableInterFilter Set.iUnion_subset Set.inter_subset_right
measure_iUnion_eq_iSup_accumulate 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder Set.accumulate Preorder.toLE	—	Set.iUnion_accumulate Monotone.measure_iUnion Set.monotone_accumulate
measure_iUnion_toMeasurable 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.iUnion toMeasurable	—	measure_iUnion_congr_of_subset subset_toMeasurable Eq.le measure_toMeasurable
measure_if 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instMembership Set.instEmptyCollection Set.indicator instZeroENNReal	—	Set.indicator_of_mem measure_empty Measure.instOuterMeasureClass Set.indicator_of_notMem
measure_inter_add_diff 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instInter Set.instSDiff	—	measure_inter_add_diff₀ MeasurableSet.nullMeasurableSet
measure_inter_conull 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl instZeroENNReal	Set.instInter	—	Set.diff_compl measure_diff_null Measure.instOuterMeasureClass
measure_inter_conull' 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instSDiff instZeroENNReal	Set.instInter	—	Set.diff_compl measure_diff_null' Set.diff_eq
measure_ne_top_iff_of_symmDiff 📖	—	—	—	—	Iff.ne measure_eq_top_iff_of_symmDiff
measure_preimage_eq_zero_iff_of_countable 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.preimage instZeroENNReal Set.instSingletonSet	—	Set.biUnion_preimage_singleton measure_biUnion_null_iff Measure.instOuterMeasureClass
measure_sUnion 📖	mathematical	Set.Pairwise Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.sUnion tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.instMembership SummationFilter.unconditional	—	Set.sUnion_eq_biUnion measure_biUnion
measure_sUnion₀ 📖	mathematical	Set.Pairwise Set AEDisjoint NullMeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.sUnion tsum Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace Set.instMembership SummationFilter.unconditional	—	Set.sUnion_eq_biUnion measure_biUnion₀
measure_symmDiff_eq 📖	mathematical	NullMeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	measure_union₀ NullMeasurableSet.diff Disjoint.aedisjoint disjoint_sdiff_sdiff
measure_symmDiff_eq_top 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Top.top instTopENNReal	symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff	—	measure_mono_top Set.subset_union_right measure_diff_eq_top
measure_symmDiff_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike symmDiff SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instSDiff Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	le_trans OuterMeasure.mono symmDiff_triangle measure_union_le Measure.instOuterMeasureClass
measure_toMeasurable_union 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion toMeasurable	—	measure_union_congr_of_subset subset_toMeasurable Eq.le measure_toMeasurable Set.Subset.rfl le_rfl
measure_union 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	measure_union₀ MeasurableSet.nullMeasurableSet Disjoint.aedisjoint
measure_union' 📖	mathematical	Disjoint Set OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice MeasurableSet	DFunLike.coe Measure ENNReal Measure.instFunLike Set.instUnion Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	measure_union₀' MeasurableSet.nullMeasurableSet Disjoint.aedisjoint
measure_union_add_inter 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instUnion Set.instInter	—	measure_inter_add_diff Set.union_inter_cancel_right Set.union_diff_right Set.inter_isAssoc Set.inter_isComm AddSemigroup.to_isAssociative AddCommMagma.to_isCommutative
measure_union_add_inter' 📖	mathematical	MeasurableSet	ENNReal Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring DFunLike.coe Measure Set Measure.instFunLike Set.instUnion Set.instInter	—	Set.union_comm Set.inter_comm measure_union_add_inter add_comm
measure_union_congr_of_subset 📖	mathematical	Set Set.instHasSubset ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike	Set.instUnion	—	Set.union_eq_iUnion measure_iUnion_congr_of_subset Bool.countable
measure_union_toMeasurable 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Set.instUnion toMeasurable	—	measure_union_congr_of_subset Set.Subset.rfl le_rfl subset_toMeasurable Eq.le measure_toMeasurable
nonempty_inter_of_measure_lt_add 📖	mathematical	MeasurableSet Set Set.instHasSubset ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	Set.Nonempty Set.instInter	—	Set.not_disjoint_iff_nonempty_inter Mathlib.Tactic.Contrapose.contrapose₃ measure_union measure_mono Measure.instOuterMeasureClass Set.union_subset
nonempty_inter_of_measure_lt_add' 📖	mathematical	MeasurableSet Set Set.instHasSubset ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Measure.instFunLike Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	Set.Nonempty Set.instInter	—	Set.inter_comm nonempty_inter_of_measure_lt_add add_comm
sum_measure_le_measure_univ 📖	mathematical	NullMeasurableSet Set.Pairwise SetLike.coe Finset Finset.instSetLike Function.onFun Set AEDisjoint	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder Finset.sum ENNReal.instAddCommMonoid DFunLike.coe Measure Measure.instFunLike Set.univ	—	measure_biUnion_finset₀ measure_mono Measure.instOuterMeasureClass Set.subset_univ
sum_measure_preimage_singleton 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	Finset.sum ENNReal ENNReal.instAddCommMonoid DFunLike.coe Measure Measure.instFunLike SetLike.coe Finset Finset.instSetLike	—	measure_biUnion_finset Set.pairwiseDisjoint_fiber Finset.set_biUnion_preimage_singleton
sum_measure_singleton 📖	mathematical	—	Finset.sum ENNReal ENNReal.instAddCommMonoid DFunLike.coe Measure Set Measure.instFunLike Set.instSingletonSet SetLike.coe Finset Finset.instSetLike	—	Finset.sum_congr sum_measure_preimage_singleton
tendsto_measure_Ici_atBot 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Ici Filter.atBot nhds ENNReal.instTopologicalSpace Set.univ	—	tendsto_measure_Iic_atTop OrderDual.instIsCountablyGeneratedAtTop
tendsto_measure_Ico_atTop 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Ico Filter.atTop nhds ENNReal.instTopologicalSpace Set.Ici	—	Set.iUnion_Ico_right tendsto_measure_iUnion_atTop Antitone.Ico antitone_const monotone_id
tendsto_measure_Iic_atTop 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Iic Filter.atTop nhds ENNReal.instTopologicalSpace Set.univ	—	Set.iUnion_Iic tendsto_measure_iUnion_atTop monotone_Iic
tendsto_measure_Ioc_atBot 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.Ioc Filter.atBot nhds ENNReal.instTopologicalSpace Set.Iic	—	Set.iUnion_Ioc_left tendsto_measure_iUnion_atBot Monotone.Ioc monotone_id antitone_const
tendsto_measure_biInter_gt 📖	mathematical	NullMeasurableSet Set Set.instHasSubset Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike nhdsWithin Set.Ioi nhds ENNReal.instTopologicalSpace Set.iInter	—	comap_coe_Ioi_nhdsGT Filter.comap.isCountablyGenerated TopologicalSpace.isCountablyGenerated_nhdsWithin FirstCountableTopology.nhds_generated_countable map_coe_Ioi_atBot Set.iInter_congr_Prop Set.biInter_eq_iInter tendsto_measure_iInter_atBot Order.not_isPredPrelimit_iff_exists_covBy CovBy.nhdsGT instClosedIciTopology OrderTopology.to_orderClosedTopology
tendsto_measure_iInter_atBot 📖	mathematical	NullMeasurableSet Monotone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike Filter.atBot nhds ENNReal.instTopologicalSpace Set.iInter	—	tendsto_measure_iInter_atTop OrderDual.instIsCountablyGeneratedAtTop Monotone.dual_left
tendsto_measure_iInter_atTop 📖	mathematical	NullMeasurableSet Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike Filter.atTop nhds ENNReal.instTopologicalSpace Set.iInter	—	Filter.Tendsto.of_neBot_imp Filter.atTop_neBot_iff Antitone.measure_iInter tendsto_atTop_iInf LinearOrder.infConvergenceClass ENNReal.instOrderTopology measure_mono Measure.instOuterMeasureClass
tendsto_measure_iInter_le 📖	mathematical	NullMeasurableSet	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.iInter Preorder.toLE Filter.atTop nhds ENNReal.instTopologicalSpace	—	Filter.Tendsto.of_neBot_imp Filter.atTop_neBot_iff measure_iInter_eq_iInf_measure_iInter_le tendsto_atTop_iInf LinearOrder.infConvergenceClass ENNReal.instOrderTopology measure_mono Measure.instOuterMeasureClass Set.biInter_subset_biInter_left le_trans
tendsto_measure_iUnion_accumulate 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Set.accumulate Preorder.toLE Filter.atTop nhds ENNReal.instTopologicalSpace Set.iUnion	—	Filter.Tendsto.of_neBot_imp Filter.atTop_neBot_iff measure_iUnion_eq_iSup_accumulate tendsto_atTop_iSup LinearOrder.supConvergenceClass ENNReal.instOrderTopology measure_mono Measure.instOuterMeasureClass Set.accumulate_subset_accumulate
tendsto_measure_iUnion_atBot 📖	mathematical	Antitone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike Filter.atBot nhds ENNReal.instTopologicalSpace Set.iUnion	—	tendsto_measure_iUnion_atTop OrderDual.instIsCountablyGeneratedAtTop Antitone.dual_left
tendsto_measure_iUnion_atTop 📖	mathematical	Monotone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	Filter.Tendsto ENNReal DFunLike.coe Measure Measure.instFunLike Filter.atTop nhds ENNReal.instTopologicalSpace Set.iUnion	—	Filter.Tendsto.of_neBot_imp Filter.atTop_neBot_iff Monotone.measure_iUnion tendsto_atTop_iSup LinearOrder.supConvergenceClass ENNReal.instOrderTopology measure_mono Measure.instOuterMeasureClass
toMeasure_apply 📖	mathematical	MeasurableSpace MeasurableSpace.instLE OuterMeasure.caratheodory MeasurableSet	DFunLike.coe Measure Set ENNReal Measure.instFunLike OuterMeasure.toMeasure OuterMeasure OuterMeasure.instFunLikeSetENNReal	—	OuterMeasure.trim_eq
toMeasure_apply₀ 📖	mathematical	MeasurableSpace MeasurableSpace.instLE OuterMeasure.caratheodory NullMeasurableSet OuterMeasure.toMeasure	DFunLike.coe Measure Set ENNReal Measure.instFunLike OuterMeasure OuterMeasure.instFunLikeSetENNReal	—	le_antisymm Measure.instOuterMeasureClass NullMeasurableSet.exists_measurable_subset_ae_eq measure_congr Filter.EventuallyEq.symm toMeasure_apply OuterMeasure.mono le_toMeasure_apply
toMeasure_toOuterMeasure 📖	mathematical	MeasurableSpace MeasurableSpace.instLE OuterMeasure.caratheodory	Measure.toOuterMeasure OuterMeasure.toMeasure OuterMeasure.trim	—	—
toOuterMeasure_toMeasure 📖	mathematical	—	OuterMeasure.toMeasure Measure.toOuterMeasure le_toOuterMeasure_caratheodory	—	Measure.ext le_toOuterMeasure_caratheodory OuterMeasure.trim_eq
tsum_meas_le_meas_iUnion_of_disjoint 📖	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	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe Measure Measure.instFunLike SummationFilter.unconditional Set.iUnion	—	tsum_meas_le_meas_iUnion_of_disjoint₀ MeasurableSet.nullMeasurableSet Disjoint.aedisjoint
tsum_meas_le_meas_iUnion_of_disjoint₀ 📖	mathematical	NullMeasurableSet Pairwise Function.onFun Set AEDisjoint	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe Measure Measure.instFunLike SummationFilter.unconditional Set.iUnion	—	ENNReal.tsum_eq_iSup_sum iSup_le_iff measure_biUnion_finset₀ measure_mono Measure.instOuterMeasureClass Set.iUnion_mono'' Set.iUnion_subset Set.Subset.rfl
tsum_measure_le_measure_univ 📖	mathematical	NullMeasurableSet Pairwise Function.onFun Set AEDisjoint	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe Measure Measure.instFunLike SummationFilter.unconditional Set.univ	—	ENNReal.tsum_eq_iSup_sum iSup_le sum_measure_le_measure_univ
tsum_measure_preimage_singleton 📖	mathematical	MeasurableSet Set.preimage Set Set.instSingletonSet	tsum ENNReal Set.Elem ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe Measure Measure.instFunLike Set.instMembership SummationFilter.unconditional	—	Set.biUnion_preimage_singleton measure_biUnion Set.pairwiseDisjoint_fiber
union_ae_eq_left_iff_ae_subset 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.instUnion Filter.EventuallyLE Prop.le	—	Measure.instOuterMeasureClass ae_le_set Set.union_diff_left ae_eq_set Filter.eventuallyLE_antisymm_iff HasSubset.Subset.eventuallyLE Set.subset_union_left
union_ae_eq_right_iff_ae_subset 📖	mathematical	—	Filter.EventuallyEq ae Measure Measure.instFunLike Measure.instOuterMeasureClass Set Set.instUnion Filter.EventuallyLE Prop.le	—	Measure.instOuterMeasureClass Set.union_comm union_ae_eq_left_iff_ae_subset

MeasureTheory.Measure

Definitions

Name	Category	Theorems
coeAddHom 📖	CompOp	1 math math: coeAddHom_apply
cofinite 📖	CompOp	8 math math: cofinite.instIsMeasurablyGenerated, mem_cofinite, MeasureTheory.cofinite_eq_bot, eventually_cofinite, MeasureTheory.UnifTight.eventually_cofinite_indicator, MeasureTheory.cofinite_eq_bot_iff, compl_mem_cofinite, cofinite_le_ae
instAdd 📖	CompOp	126 math math: InnerRegular.instHAdd, MeasurableEmbedding.comap_add, MeasureTheory.lintegral_add_measure, MeasureTheory.isFiniteMeasureAdd, MeasureTheory.DominatedFinMeasAdditive.add_measure_left, rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular, rnDeriv_add_of_mutuallySingular, AbsolutelyContinuous.add_left, comp_add, measure_toMeasurable_add_inter_right, map_add, MeasureTheory.integral_add_measure, ProbabilityTheory.Kernel.coe_add, ProbabilityTheory.boolKernel_comp_measure, instMeasurableAdd₂, MeasureTheory.AEStronglyMeasurable.add_measure, measure_toMeasurable_add_inter_left, restrict_add, MeasureTheory.instSFiniteHAddMeasure, restrict_add_restrict_compl, MutuallySingular.add_left, MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity, conv_add, MeasureTheory.VAddInvariantMeasure.add, add_right_inj, add_comp, haveLebesgueDecomposition_add, MeasureTheory.nndist_integral_add_measure_le_lintegral, AEMeasurable.add_measure, sum_add_sum_compl, MeasureTheory.ae_add_measure_iff, AbsolutelyContinuous.add_left_iff, MeasureTheory.SignedMeasure.singularPart_totalVariation, singularPart_def, rnDeriv_add_singularPart, ProbabilityTheory.setBernoulli_apply', restrict_inter_add_diff₀, MeasureTheory.MeasurePreserving.add_measure, sub_le_iff_le_add, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, restrict_union, restrict_union', MeasureTheory.IntegrableOn.add_measure, sub_le_iff_le_add_of_le, add_comp', MeasureTheory.FiniteMeasure.toMeasure_add, MeasureTheory.measureReal_add_apply, ProbabilityTheory.mgf_add_measure, sub_add_cancel_of_le, restrict_union_add_inter, MeasureTheory.withDensity_add_left, MeasureTheory.SMulInvariantMeasure.add, add_apply, MeasureTheory.eLpNorm_le_add_measure_left, rnDeriv_add, add_sub_cancel, sum_cond, MeasureTheory.eLpNorm_le_add_measure_right, ae_eq_or_eq_iff_eq_dirac_add_dirac, MeasureTheory.Integrable.add_measure, coe_add, AbsolutelyContinuous.add_right, rnDeriv_add_right_of_mutuallySingular', ProbabilityTheory.Kernel.add_apply, MeasureTheory.weightedSMul_add_measure, HaveLebesgueDecomposition.lebesgue_decomposition, add_mconv, toSignedMeasure_add, restrict_union₀, sum_add_sum, toENNRealVectorMeasure_add, add_top, MeasureTheory.integrableOn_add_measure, fst_add, rnDeriv_def, aestronglyMeasurable_add_measure_iff, MeasureTheory.Add.sigmaFinite, MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm, restrict_union_add_inter₀, MutuallySingular.add_right, MutuallySingular.add_left_iff, MeasureTheory.average_add_measure, MeasureTheory.hasFiniteIntegral_add_measure, prod_add, MeasureTheory.SignedMeasure.jordanDecomposition_add_withDensity_mutuallySingular, MeasureTheory.integrable_add_measure, MeasureTheory.withDensity_add_measure, sum_bool, compProd_add_left, StieltjesFunction.measure_add, MeasureTheory.SimpleFunc.lintegral_add, ProbabilityTheory.Kernel.const_add, AbsolutelyContinuous.add, add_left_inj, MeasureTheory.withDensity_add_right, le_add_right, le_add_left, sub_def, singularPart_add_rnDeriv, add_prod, restrict_union_add_inter', snd_add, compProd_add_right, MeasureTheory.laverage_add_measure, MeasureTheory.eLpNorm_one_add_measure, add_sub_of_mutuallySingular, HaveLebesgueDecomposition.add_left, MeasureTheory.HasFiniteIntegral.add_measure, top_add, aemeasurable_add_measure_iff, rnDeriv_add', mconv_add, restrict_union_le, ProbabilityTheory.setBernoulli_apply, restrict_compl_add_restrict, haveLebesgueDecomposition_spec, add_conv, add_toOuterMeasure, support_add, singularPart_add, MeasureTheory.DominatedFinMeasAdditive.add_measure_right, MeasureTheory.trim_add, MutuallySingular.add_right_iff, restrict_inter_add_diff, ProbabilityTheory.setBernoulli_eq_map, rnDeriv_add_right_of_mutuallySingular
instAddCommMonoid 📖	CompOp	52 math math: ProbabilityTheory.Kernel.coe_nsmul, MeasureTheory.instIsFiniteMeasureSumMeasure, MeasureTheory.integral_domSMul, MeasureTheory.addHaarScalarFactor_smul_inv_eq_distribHaarChar, instIsOrderedAddMonoid, ae_mem_finset_iff, ProbabilityTheory.sum_meas_smul_cond_fiber, domSMul_apply, comapₗ_eq_comap, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar_inv, ae_mem_finset_iff_map_eq_sum_dirac, ProbabilityTheory.Kernel.nsmul_apply, ProbabilityTheory.Kernel.coeAddHom_apply, IsAddHaarMeasure.domSMul, InnerRegular.instSum, sum_fintype, MeasureTheory.addHaarScalarFactor_smul_eq_distribHaarChar, comapₗ_apply, mapₗ_congr, coeAddHom_apply, addHaarScalarFactor_smul_congr, Ergodic.iff_mem_extremePoints_measure_univ_eq, MeasureTheory.distribHaarChar_apply, map_def, MeasureTheory.integral_finset_sum_measure, finset_sum_apply, mapₗ_mk_apply_of_aemeasurable, Regular.domSMul, instSMulCommClassDomMulActNNReal, le_liftLinear_apply, ProbabilityTheory.Kernel.coe_finset_sum, MeasureTheory.ae_finsetSum_measure_iff, coe_finset_sum, instSMulCommClassNNRealDomMulAct, mapₗ_apply_of_measurable, liftLinear_apply, Ergodic.iff_mem_extremePoints, MeasureTheory.lintegral_finset_sum_measure, ProbabilityTheory.Kernel.finset_sum_apply, Ergodic.mem_extremePoints_measure_univ_eq, mapₗ_eq_zero_iff, MeasureTheory.SimpleFunc.lintegral_finset_sum, addHaarScalarFactor_domSMul, restrictₗ_apply, addHaarScalarFactor_smul_congr', sum_restrict_le, MeasureTheory.integrable_finset_sum_measure, Ergodic.mem_extremePoints, MeasureTheory.FiniteMeasure.toMeasure_sum, MeasureTheory.FiniteMeasure.toMeasureAddMonoidHom_apply, instModuleIsTorsionFree, sum_coe_finset
instCompleteLattice 📖	CompOp	11 math math: sub_top, mutuallySingular_tfae, mkMetric_top, disjoint_of_disjoint_ae, mutuallySingular_iff_disjoint, inf_apply, add_top, toOuterMeasure_top, MutuallySingular.disjoint, top_add, MeasureTheory.OuterMeasure.toMeasure_top
instCompleteSemilatticeInf 📖	CompOp	—
instDistribMulAction 📖	CompOp	—
instInfSet 📖	CompOp	3 math math: restrict_sInf_eq_sInf_restrict, sInf_apply, sub_def
instInhabited 📖	CompOp	—
instModule 📖	CompOp	11 math math: comapₗ_eq_comap, comapₗ_apply, mapₗ_congr, map_def, mapₗ_mk_apply_of_aemeasurable, le_liftLinear_apply, mapₗ_apply_of_measurable, liftLinear_apply, mapₗ_eq_zero_iff, restrictₗ_apply, instModuleIsTorsionFree
instMulAction 📖	CompOp	—
instPartialOrder 📖	CompOp	41 math math: mutuallySingular_tfae, instIsOrderedAddMonoid, toSignedMeasure_le_toSignedMeasure_iff, MeasureTheory.sfiniteSeq_le, le_mkMetric, restrict_biUnion_le, mkMetric_mono, sub_le_iff_le_add, withDensity_rnDeriv_le, nonpos_iff_eq_zero', le_iff', restrict_mono_set, lt_iff', disjoint_of_disjoint_ae, singularPart_le, mutuallySingular_iff_disjoint, le_hausdorffMeasure, MeasureTheory.IsHahnDecomposition.ge_on_compl, MeasureTheory.withDensity_inv_same_le, IicSnd_le_fst, restrict_mono_ae, ProbabilityTheory.Kernel.withDensity_rnDeriv_le, zero_le, restrict_le_self, MeasureTheory.withDensity_pdf_le_map, le_iff, toOuterMeasure_le, le_sum, sub_def, IicSnd_mono, sub_le, MutuallySingular.disjoint, MeasureTheory.withDensity_mono, sum_restrict_le, restrict_union_le, le_intro, lt_iff, MeasureTheory.IsHahnDecomposition.le_on, mkMetric_mono_smul, rnDeriv_le_one_iff_le, restrict_iUnion_le
instSMul 📖	CompOp	240 math math: MutuallySingular.smul_nnreal, MeasureTheory.SMulInvariantMeasure.smul, IsHaarMeasure.nnreal_smul, restrict_singleton, isAddInvariant_eq_smul_of_compactSpace, IsEverywherePos.smul_measure, join_smul, restrict_smul, ae_ennreal_smul_measure_eq, MeasureTheory.integral_smul_nnreal_measure, Real.smul_map_volume_mul_right, IsAddHaarMeasure.smul, WeaklyRegular.smul_nnreal, AbsolutelyContinuous.smul_left, rnDeriv_smul_right', AddCircle.volume_eq_smul_haarAddCircle, ae_mem_finset_iff, MeasureTheory.FinMeasAdditive.smul_measure, ProbabilityTheory.boolKernel_comp_measure, MeasureTheory.lintegral_smul_measure, haveLebesgueDecompositionSMul, MeasureTheory.tilted_neg_same', ProbabilityTheory.sum_meas_smul_cond_fiber, coe_nnreal_smul_apply, MeasureTheory.restrict_compl_sigmaFiniteSet, haarMeasure_unique, MeasureTheory.eLpNorm_smul_measure_of_ne_top', rnDeriv_smul_right, rnDeriv_smul_left_of_ne_top', sum_smul_dirac, ae_mem_finset_iff_map_eq_sum_dirac, haarScalarFactor_smul, OuterRegular.smul_nnreal, Real.smul_map_diagonal_volume_pi, map_fst_prod, const_comp, MeasureTheory.laverage_eq', MeasureTheory.AEStronglyMeasurable.smul_measure, Ergodic.eq_smul_of_absolutelyContinuous, essSup_ennreal_smul_measure, InnerRegular.smul, integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, QuasiErgodic.smul_measure, MeasureTheory.isProbabilityMeasureSMul, comp_eq_sum_of_countable, LinearMap.exists_map_addHaar_eq_smul_addHaar, discard_comp, rnDeriv_smul_left_of_ne_top, Real.map_matrix_volume_pi_eq_smul_volume_pi, Real.smul_map_volume_mul_left, map_linearMap_addHaar_eq_smul_addHaar, MeasureTheory.lpNorm_smul_measure_of_ne_zero, MeasureTheory.NullMeasurableSet.smul_measure, ProbabilityTheory.setBernoulli_apply', QuasiMeasurePreserving.smul_measure, Ergodic.iff_mem_extremePoints_measure_univ_eq, MeasureTheory.instSFiniteHSMulENNRealMeasure, MeasureTheory.mulEquivHaarChar_smul_map, MeasureTheory.isAddLeftInvariant_smul, ae_eq_or_eq_iff_map_eq_dirac_add_dirac, Regular.smul, MeasureTheory.eLpNorm_one_smul_measure, MeasureTheory.MeasurePreserving.smul_measure, MutuallySingular.smul, PreErgodic.smul_measure, MeasureTheory.SMul.sigmaFinite, addHaarMeasure_unique, MeasureTheory.isMulLeftInvariant_smul, isMulLeftInvariant_eq_smul_of_innerRegular, MeasureTheory.isFiniteMeasureSMulOfNNRealTower, rnDeriv_smul_left', pi_map_eval, MeasureTheory.isMulRightInvariant_smul, MeasureTheory.eLpNorm'_smul_measure, MeasureTheory.eLpNorm_smul_measure_of_ne_top, ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul, isMulLeftInvariant_eq_smul_of_regular, smul_toOuterMeasure, MeasureTheory.FinMeasAdditive.smul_measure_iff, map_eq_sum, rnDeriv_smul_right_of_ne_top', MeasureTheory.integrable_smul_measure, MeasureTheory.setLAverage_eq', ProbabilityTheory.Kernel.instIsIrreducibleHSMulENNRealMeasure, MeasureTheory.nullMeasurableSet_smul_measure_iff, toSignedMeasure_smul, intervalIntegral.integral_smul_measure, MeasureTheory.MemLp.smul_measure, ae_eq_or_eq_iff_eq_dirac_add_dirac, conv_smul_left, ProbabilityTheory.Kernel.IsProper.restrict_eq_indicator_smul', isOpenPosMeasure_smul, MeasureTheory.setAverage_eq', Ergodic.smul_measure, ProbabilityTheory.Kernel.comp_discard', ae_smul_measure_iff, instSMulCommClassDomMulActNNReal, MeasureTheory.eLpNormEssSup_smul_measure, MeasureTheory.Integrable.to_average, MeasureTheory.tilted_const', isMulInvariant_eq_smul_of_compactSpace, exists_integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, MeasureTheory.measure_eq_div_smul, smul_absolutelyContinuous, MeasureTheory.JordanDecomposition.smul_posPart, ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul, coe_smul, smul_finite, MeasureTheory.SimpleFunc.lintegral_smul, ae_ennreal_smul_measure_iff, addHaarScalarFactor_smul_smul, MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg, MeasureTheory.IsFiniteMeasure.average, absolutelyContinuous_smul, MeasureTheory.count_withDensity, bind_smul, MeasureTheory.FiniteMeasure.toMeasure_normalize_eq_of_nonzero, MeasureTheory.IsFiniteMeasureOnCompacts.smul_nnreal, exists_sum_smul_dirac, MeasureTheory.measureReal_ennreal_smul_apply, InnerRegularWRT.smul, comap_smul, instSMulCommClassNNRealDomMulAct, MeasureTheory.IsFiniteMeasureOnCompacts.smul, MeasureTheory.count_withDensity', map_right_mul_eq_modularCharacterFun_smul, MeasureTheory.addEquivAddHaarChar_smul_map, Measurable.smul_measure, MeasureTheory.isMulLeftInvariant_smul_nnreal, MeasureTheory.instIsProbabilityMeasureHAddMeasureHSMulNNRealToNNRealSymm, Real.map_linearMap_volume_pi_eq_smul_volume_pi, map_linearMap_addHaar_pi_eq_smul_addHaar, aemeasurable_smul_measure_iff, MeasureTheory.isAddRightInvariant_smul, mul_addHaarScalarFactor_smul, map_addHaar_smul, integral_isMulLeftInvariant_eq_smul_of_hasCompactSupport, ae_smul_measure, MeasureTheory.inv_measure_univ_smul_eq_self, isMulLeftInvariant_eq_smul, MeasureTheory.VAddInvariantMeasure.vadd_nnreal, IsHaarMeasure.smul, InnerRegular.smul_nnreal, Ergodic.iff_mem_extremePoints, MeasureTheory.HasFiniteIntegral.smul_measure, MeasureTheory.JordanDecomposition.smul_negPart, MeasureTheory.isAddRightInvariant_smul_nnreal, mconv_smul_right, MeasureTheory.SMulInvariantMeasure.smul_nnreal, prod_smul_right, MeasureTheory.JordanDecomposition.real_smul_posPart_neg, isAddLeftInvariant_eq_smul_of_regular, WeaklyRegular.smul, MeasureTheory.measure_eq_sub_vadd, IsFundamentalDomain.QuotientMeasureEqMeasurePreimage_smulHaarMeasure, OuterRegular.smul, smul_apply, MeasureTheory.average_eq', MeasureTheory.tilted_zero', MeasureTheory.addEquivAddHaarChar_smul_eq_comap, ae_smul_measure_le, MeasureTheory.mulEquivHaarChar_smul_eq_comap, comp_smul, isAddLeftInvariant_eq_smul_of_innerRegular, MeasureTheory.JordanDecomposition.real_smul_negPart_neg, Ergodic.mem_extremePoints_measure_univ_eq, map_const, AlternatingMap.measure_def, MeasureTheory.dirac_withDensity', Real.map_volume_mul_right, haarScalarFactor_smul_smul, rnDeriv_smul_left, instIsScalarTower, exists_integral_isAddLeftInvariant_eq_smul_of_hasCompactSupport, StieltjesFunction.measure_smul, MeasureTheory.Integrable.smul_measure, Regular.smul_nnreal, MeasureTheory.isZeroOrProbabilityMeasureSMul, MeasureTheory.setLIntegral_smul_measure, MeasureTheory.isLocallyFiniteMeasureSMulNNReal, MeasureTheory.FiniteMeasure.toMeasure_smul, AbsolutelyContinuous.smul, essSup_smul_measure, MeasureTheory.isFiniteMeasureSMulNNReal, MeasureTheory.Integrable.smul_measure_nnreal, MeasureTheory.withDensity_smul_measure, MeasureTheory.restrict_compl_sigmaFiniteSetWRT, map_smul, InnerRegularCompactLTTop.smul_nnreal, ennreal_smul_eq_zero, IsEverywherePos.smul_measure_nnreal, MeasureTheory.withDensity_smul, haveLebesgueDecompositionSMulRight, IsAddHaarMeasure.nnreal_smul, compProd_smul_left, mul_haarScalarFactor_smul, MeasureTheory.llr_smul_right, AEMeasurable.smul_measure, MeasureTheory.integrable_average, MeasureTheory.lpNorm_smul_measure_of_ne_top, mconv_smul_left, instSMulCommClass, MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg, MeasureTheory.eLpNorm_smul_measure_of_ne_zero, MeasureTheory.isMulRightInvariant_smul_nnreal, instIsCentralScalar, ProbabilityTheory.mgf_smul_measure, MeasureTheory.isAddLeftInvariant_smul_nnreal, map_right_add_eq_addModularCharacterFun_vadd, MeasureTheory.weightedSMul_smul_measure, MeasureTheory.VAddInvariantMeasure.vadd, MeasureTheory.eLpNorm_smul_measure_of_ne_zero', MeasureTheory.withDensity_const, singularPart_smul_right, MeasureTheory.eLpNormEssSup_ennreal_smul_measure, Ergodic.mem_extremePoints, isAddLeftInvariant_eq_smul, ProbabilityTheory.setBernoulli_apply, ProbabilityTheory.Kernel.const_comp, MeasureTheory.integrable_inv_smul_measure, MeasureTheory.integral_smul_measure, conv_smul_right, addHaarScalarFactor_smul, MeasureTheory.withDensity_smul', MeasureTheory.llr_smul_left, map_snd_prod, singularPart_smul, LinearMap.exists_map_addHaar_eq_smul_addHaar', rnDeriv_smul_right_of_ne_top, InnerRegularCompactLTTop.smul, mkMetric_mono_smul, MeasureTheory.measureReal_nnreal_smul_apply, ae_smul_measure_eq, prod_smul_left, haveLebesgueDecompositionSMul', ProbabilityTheory.setBernoulli_eq_map, bind_const, IsFundamentalDomain.AddQuotientMeasureEqMeasurePreimage_vaddAddHaarMeasure, MeasureTheory.dirac_withDensity, Real.map_volume_mul_left
instZero 📖	CompOp	185 math math: comap_undef, rnDeriv_zero, MeasureTheory.restrict_dirac', MeasureTheory.isFiniteMeasureZero, MeasureTheory.IsFundamentalDomain.quotientMeasureEqMeasurePreimage_of_zero, sub_top, MeasureTheory.unifIntegrable_zero_meas, MeasureTheory.hasFiniteIntegral_zero_measure, WeaklyRegular.zero, conv_zero, StieltjesFunction.measure_zero, MeasureTheory.average_zero_measure, ProbabilityTheory.Kernel.indep_zero_right, singularPart_eq_zero, Ergodic.zero_measure, restrict_empty, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, restrict_singleton', AbsolutelyContinuous.zero, MeasureTheory.IsProbabilityMeasure.neZero, snd_zero, MeasureTheory.condExpL1_measure_zero, MeasureTheory.withDensity_eq_zero_iff, MeasureTheory.withDensity_zero, ProbabilityTheory.Kernel.coe_zero, instHaveLebesgueDecompositionZeroRight, ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectROfProdMk, OuterRegular.zero, essInf_measure_zero, ProbabilityTheory.covarianceOperator_zero, restrict_eq_zero, MeasureTheory.ae_zero, MeasureTheory.memLp_measure_zero, MeasureTheory.aestronglyMeasurable_zero_measure, singularPart_def, MeasureTheory.eLpNorm'_measure_zero_of_pos, MeasureTheory.restrict_dirac, MeasureTheory.laverage_zero_measure, ProbabilityTheory.uniformOn_eq_zero, MeasureTheory.SignedMeasure.totalVariation_zero, instNeZeroOfNonempty, MeasureTheory.lpNorm_measure_zero, zero_toOuterMeasure, InformationTheory.klDiv_zero_right, ProbabilityTheory.covarianceBilin_zero, eq_zero_of_absolutelyContinuous_of_mutuallySingular, MeasureTheory.measureReal_zero, ProbabilityTheory.cond_eq_zero_of_meas_eq_zero, MeasureTheory.JordanDecomposition.zero_posPart, map_def, MeasureTheory.zero_trim, nonpos_iff_eq_zero', InformationTheory.klDiv_zero_left, ProbabilityTheory.covarianceBilinDual_zero, MeasureTheory.measureUnivNNReal_eq_zero, ProbabilityTheory.Kernel.iIndepFun_zero_right, MeasureTheory.instSFiniteOfNatMeasure, ProbabilityTheory.avgRisk_zero_prior, map_eq_zero_iff, MeasureTheory.SMulInvariantMeasure.zero, restrict.neZero, ProbabilityTheory.centralMoment_zero_measure, MeasureTheory.IsProjectiveMeasureFamily.eq_zero_of_isEmpty, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_apply_eq_zero, ProbabilityTheory.variance_zero_measure, singularPart_zero_right, withDensity_rnDeriv_eq_zero, MeasureTheory.uniformIntegrable_zero_meas, MutuallySingular.restrict_nullSet, ProbabilityTheory.mgf_zero_measure, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_measure_eq_zero, ProbabilityTheory.uniformOn_empty_meas, zero_prod, zero_conv, bind_zero_right, ProbabilityTheory.Kernel.compProd_eq_zero_iff, ProbabilityTheory.Kernel.indepSet_zero_right, singularPart_withDensity, MeasureTheory.SimpleFunc.lintegral_zero, MutuallySingular.zero_left, MeasureTheory.ae_eq_bot, MeasureTheory.JordanDecomposition.zero_negPart, singularPart_self, MeasureTheory.toFinite_eq_zero_iff, ProbabilityTheory.Kernel.instNeZeroMeasureCoeSectLOfProdMk, restrict_zero, MutuallySingular.zero_right, ProbabilityTheory.Kernel.indepSets_zero_right, essSup_measure_zero, MeasureTheory.lintegral_zero_measure, compProd_zero_left, ProbabilityTheory.moment_zero_measure, ProbabilityTheory.Kernel.const_zero, zero_le, sub_eq_zero_of_le, MeasureTheory.tilted_zero_measure, ProbabilityTheory.covariance_zero_measure, singularPart_zero, MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure, ProbabilityTheory.Kernel.iIndepSets_zero_right, MeasureTheory.eLpNorm'_measure_zero_of_neg, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_mutuallySingular, ProbabilityTheory.Kernel.iIndep_zero_right, ProbabilityTheory.Kernel.withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, ProbabilityTheory.Kernel.singularPart_eq_zero_iff_absolutelyContinuous, sum_eq_zero, MeasureTheory.IsAddFundamentalDomain.addQuotientMeasureEqMeasurePreimage_of_zero, MeasureTheory.charFun_zero_measure, restrict_zero_set, MeasureTheory.tilted_of_not_integrable, MeasureTheory.VAddInvariantMeasure.zero, MeasureTheory.eq_zero_or_isProbabilityMeasure, aemeasurable_zero_measure, MeasureTheory.measureUnivNNReal_zero, ProbabilityTheory.uncenteredCovarianceBilin_zero, zero_mconv, sum_zero, eq_zero_of_isEmpty, support_zero, absolutelyContinuous_zero_iff, ProbabilityTheory.cond_eq_zero, QuasiErgodic.zero_measure, mapₗ_eq_zero_iff, MeasureTheory.null_iff_of_isAddLeftInvariant, MutuallySingular.self_iff, MeasureTheory.OuterMeasure.toMeasure_zero, ProbabilityTheory.cond_empty, MeasureTheory.sfiniteSeq_zero, MeasureTheory.Lp.norm_measure_zero, sum_of_isEmpty, compProd_of_not_sfinite, ProbabilityTheory.Kernel.zero_apply, MeasureTheory.integral_zero_measure, MutuallySingular.restrict_compl_nullSet, compProd_zero_right, compProd_of_not_isSFiniteKernel, MeasureTheory.integrable_zero_measure, ProbabilityTheory.Kernel.indepFun_zero_right, ennreal_smul_eq_zero, MeasureTheory.measureReal_zero_apply, zero_sub, compProd_eq_zero_iff, Real.hausdorffMeasure_of_finrank_lt, MeasureTheory.eLpNorm'_measure_zero_of_exponent_zero, ProbabilityTheory.bayesRisk_zero_right, MeasureTheory.null_iff_of_isMulLeftInvariant, measure_univ_eq_zero, sub_self, bind_zero_right', prod_zero, toSphere_eq_zero_iff_finrank, map_zero, fst_zero, MeasureTheory.FiniteMeasure.toMeasure_zero, join_zero, MeasureTheory.tilted_of_not_aemeasurable, bind_zero_left, singularPart_of_not_haveLebesgueDecomposition, MeasureTheory.eLpNormEssSup_measure_zero, toSignedMeasure_zero, ProbabilityTheory.cgf_zero_measure, mconv_zero, MeasureTheory.OuterMeasure.toMeasure_eq_zero, ProbabilityTheory.evariance_zero_measure, map_of_not_aemeasurable, MeasureTheory.eLpNorm_measure_zero, MeasureTheory.weightedSMul_zero_measure, toENNRealVectorMeasure_zero, singularPart_eq_zero_of_ac, instHaveLebesgueDecompositionZeroLeft, PreErgodic.zero_measure, MeasureTheory.toFinite_zero, ProbabilityTheory.uncenteredCovarianceBilinDual_zero, ProbabilityTheory.Kernel.iIndepSet_zero_right, coe_zero, comap_zero, sub_zero, Regular.zero, StieltjesFunction.measure_const, toSphere_eq_zero_iff, MeasureTheory.withDensity_zero_left, ProbabilityTheory.Kernel.HasSubgaussianMGF.zero_measure, ProbabilityTheory.uniformOn_eq_zero', InnerRegular.zero, sum_extend_zero
sum 📖	CompOp	75 math math: sum_apply_eq_zero', sum_sum, MeasureTheory.instSFiniteSumOfCountable, MeasureTheory.SimpleFunc.lintegral_sum, aestronglyMeasurable_sum_measure_iff, MeasureTheory.IsAddFundamentalDomain.sum_restrict, MeasureTheory.AEStronglyMeasurable.sum_measure, sum_smul_dirac, le_sum_apply, sum_apply_of_countable, ae_sum_iff, comp_eq_sum_of_countable, sum_add_sum_compl, sum_fintype, restrict_sum_of_countable, ProbabilityTheory.Kernel.sum_const, MeasureTheory.hasSum_lintegral_measure, join_sum, ae_sum_eq, sum_comm, MeasureTheory.withDensity_sum, sum_comp_equiv, restrict_biUnion_le, MeasureTheory.IsFundamentalDomain.sum_restrict, restrict_iUnion, sum_apply, snd_sum, MeasureTheory.withDensity_tsum, map_eq_sum, InnerRegular.instSum_1, sum_cond, compProd_sum_left, AEMeasurable.sum_measure, MeasureTheory.sum_sfiniteSeq, restrict_sum, sum_apply_eq_zero, sum_add_sum, MeasureTheory.count_withDensity, MeasureTheory.sum.sigmaFinite, exists_sum_smul_dirac, MeasureTheory.count_withDensity', restrict_biUnion_finset, HaveLebesgueDecomposition.sum_left, restrict_iUnion_ae, ProbabilityTheory.Kernel.sum_apply, MutuallySingular.sum_right, prod_sum_right, MeasureTheory.IsAddFundamentalDomain.sum_restrict_of_ac, restrict_biUnion, sum_eq_zero, sum_bool, aemeasurable_sum_measure_iff, sum_congr, le_sum, MeasureTheory.IsFundamentalDomain.sum_restrict_of_ac, prod_sum, sum_zero, ProbabilityTheory.Kernel.measure_sum_seq, compProd_sum_right, sum_of_isEmpty, MeasureTheory.sfinite_sum_of_countable, prod_sum_left, MeasureTheory.instIsFiniteMeasureSumOfFinite, absolutelyContinuous_sum_left, fst_sum, MutuallySingular.sum_left, absolutelyContinuous_sum_right, sum_restrict_le, MeasureTheory.SFinite.out', MeasureTheory.lintegral_sum_measure, ae_sum_iff', MeasureTheory.sum_restrict_disjointed_spanningSets, sum_coe_finset, restrict_iUnion_le, sum_extend_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—
add_toOuterMeasure 📖	mathematical	—	toOuterMeasure MeasureTheory.Measure instAdd MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instAdd	—	—
add_top 📖	mathematical	—	MeasureTheory.Measure instAdd Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique le_add_left le_rfl
ae_ennreal_smul_measure_eq 📖	mathematical	—	MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	Filter.ext instOuterMeasureClass IsScalarTower.right ae_ennreal_smul_measure_iff
ae_ennreal_smul_measure_iff 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass ENNReal instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right	—	instOuterMeasureClass IsScalarTower.right ENNReal.instNoZeroDivisors
ae_smul_measure 📖	mathematical	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	instSMul	—	instOuterMeasureClass MeasureTheory.ae_iff smul_apply smul_one_smul smul_zero
ae_smul_measure_eq 📖	mathematical	—	MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass instSMul SMulZeroClass.toSMul ENNReal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ENNReal.instAddCommMonoid	—	Filter.ext instOuterMeasureClass ae_smul_measure_iff
ae_smul_measure_iff 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass instSMul SMulZeroClass.toSMul ENNReal AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction ENNReal.instAddCommMonoid	—	instOuterMeasureClass IsDomain.toIsCancelMulZero
ae_smul_measure_le 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass instSMul	—	instOuterMeasureClass ae_smul_measure
ae_sum_eq 📖	mathematical	—	MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass sum iSup Filter Filter.instSupSet	—	Filter.ext instOuterMeasureClass ae_sum_iff Filter.mem_iSup
ae_sum_iff 📖	mathematical	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass sum	—	sum_apply_eq_zero
ae_sum_iff' 📖	mathematical	MeasurableSet setOf	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass sum	—	sum_apply_eq_zero' MeasurableSet.compl
apply_eq_zero_of_isEmpty 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instZeroENNReal	—	Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.measure_empty instOuterMeasureClass
coeAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom MeasureTheory.Measure AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addZeroClass Set ENNReal AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddMonoidHom.instFunLike coeAddHom instFunLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instAdd Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	—
coe_finset_sum 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Finset.sum instAddCommMonoid Pi.addCommMonoid ENNReal.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
coe_nnreal_smul_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike NNReal instSMul Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.ofNNReal	—	IsScalarTower.right
coe_smul 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instSMul Function.hasSMul	—	—
coe_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instZero Pi.instZero instZeroENNReal	—	—
cofinite_le_ae 📖	mathematical	—	Filter Preorder.toLE PartialOrder.toPreorder Filter.instPartialOrder cofinite MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	—	instOuterMeasureClass
compl_mem_cofinite 📖	mathematical	—	Set Filter Filter.instMembership cofinite Compl.compl Set.instCompl ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike Top.top instTopENNReal	—	mem_cofinite compl_compl
ennreal_smul_eq_zero 📖	mathematical	—	ENNReal MeasureTheory.Measure instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right instZero instZeroENNReal	—	IsScalarTower.right ENNReal.instNoZeroDivisors
eq_zero_of_isEmpty 📖	mathematical	—	MeasureTheory.Measure instZero	—	instSubsingleton
eventually_cofinite 📖	mathematical	—	Filter.Eventually cofinite ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike setOf Top.top instTopENNReal	—	—
finset_sum_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Finset.sum instAddCommMonoid ENNReal.instAddCommMonoid	—	coe_finset_sum Finset.sum_apply
inf_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice instCompleteLattice InfSet.sInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder setOf Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Set.instInter Compl.compl Set.instCompl	—	sInf_pair sInf_apply MeasureTheory.OuterMeasure.sInf_apply Set.image_nonempty Set.insert_nonempty le_antisymm le_sInf LE.le.trans iInf₂_le Set.mem_iUnion iInf_image iInf_congr_Prop iInf_pair ENNReal.tsum_eq_add_tsum_ite zero_ne_one Summable.tsum_eq_zero_iff ENNReal.instIsOrderedAddMonoid ENNReal.instCanonicallyOrderedAdd OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.summable MeasureTheory.measure_empty instOuterMeasureClass inf_of_le_left add_zero add_le_add IsOrderedAddMonoid.toAddLeftMono covariant_swap_add_of_covariant_add inf_le_left inf_le_right le_iInf₂ MeasureTheory.measure_mono Set.inter_subset_left MeasureTheory.measure_biUnion_le Set.to_countable SetCoe.countable instCountableNat Set.compl_iUnion Set.mem_iUnion₂ Set.mem_iInter₂ Set.ext tsum_univ Summable.tsum_union_disjoint ENNReal.instT2Space ENNReal.instContinuousAdd Set.disjoint_iff LT.lt.not_ge Set.mem_setOf_eq Eq.le tsum_congr inf_of_le_right le_of_lt le_trans sInf_le
instIsCentralScalar 📖	mathematical	—	IsCentralScalar MeasureTheory.Measure instSMul MulOpposite IsScalarTower.op_left ENNReal Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id	—	IsScalarTower.op_left ext IsCentralScalar.op_smul_eq_smul
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid MeasureTheory.Measure instAddCommMonoid instPartialOrder	—	add_le_add_left covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid
instIsScalarTower 📖	mathematical	—	IsScalarTower MeasureTheory.Measure instSMul	—	ext smul_assoc
instModuleIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree MeasureTheory.Measure instAddCommMonoid instModule	—	Function.Injective.moduleIsTorsionFree Pi.instModuleIsTorsionFree DFunLike.coe_injective
instNeZeroENNRealCoeSetUniv 📖	mathematical	—	ENNReal instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike Set.univ	—	measure_univ_ne_zero
instSMulCommClass 📖	mathematical	—	SMulCommClass MeasureTheory.Measure instSMul	—	ext SMulCommClass.smul_comm
instSubsingleton 📖	mathematical	—	MeasureTheory.Measure	—	ext apply_eq_zero_of_isEmpty
le_add_left 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	instAdd	—	le_add_left ENNReal.instCanonicallyOrderedAdd
le_add_right 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	instAdd	—	le_add_right ENNReal.instCanonicallyOrderedAdd
le_iff 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLike	—	outerMeasure_le_iff
le_iff' 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLike	—	—
le_intro 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set instFunLike	instPartialOrder	—	le_iff Set.eq_empty_or_nonempty MeasureTheory.measure_empty instOuterMeasureClass
le_sum 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder sum	—	le_iff sum_apply ENNReal.le_tsum
le_sum_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace DFunLike.coe MeasureTheory.Measure Set instFunLike SummationFilter.unconditional sum	—	MeasureTheory.le_toMeasure_apply
lt_iff 📖	mathematical	—	MeasureTheory.Measure Preorder.toLT PartialOrder.toPreorder instPartialOrder Preorder.toLE MeasurableSet ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLike	—	lt_iff_le_not_ge
lt_iff' 📖	mathematical	—	MeasureTheory.Measure Preorder.toLT PartialOrder.toPreorder instPartialOrder Preorder.toLE ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLike	—	lt_iff_le_not_ge
measure_eq_left_of_subset_of_measure_add_eq 📖	—	Set Set.instHasSubset DFunLike.coe MeasureTheory.Measure ENNReal instFunLike instAdd	—	—	le_antisymm MeasureTheory.measure_mono instOuterMeasureClass add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid ENNReal.le_of_add_le_add_right ne_top_of_le_ne_top le_add_left ENNReal.instCanonicallyOrderedAdd le_rfl
measure_eq_right_of_subset_of_measure_add_eq 📖	—	Set Set.instHasSubset DFunLike.coe MeasureTheory.Measure ENNReal instFunLike instAdd	—	—	measure_eq_left_of_subset_of_measure_add_eq add_comm
measure_inter_eq_of_ae 📖	mathematical	Filter.Eventually Set Set.instMembership MeasureTheory.ae MeasureTheory.Measure instFunLike instOuterMeasureClass	DFunLike.coe ENNReal Set.instInter	—	instOuterMeasureClass le_antisymm MeasureTheory.measure_mono Set.inter_subset_right Filter.EventuallyLE.measure_le Filter.mp_mem Filter.univ_mem'
measure_inter_eq_of_measure_eq 📖	mathematical	MeasurableSet DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instHasSubset	Set.instInter	—	le_antisymm MeasureTheory.measure_mono instOuterMeasureClass Set.inter_subset_inter subset_refl Set.instReflSubset MeasureTheory.measure_inter_add_diff add_le_add_right IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid Set.diff_subset_diff LT.lt.ne lt_of_le_of_lt Set.diff_subset Ne.lt_top ENNReal.le_of_add_le_add_right
measure_mono_both 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder Set Set.instHasSubset	ENNReal ENNReal.instPartialOrder DFunLike.coe instFunLike	—	LE.le.trans MeasureTheory.measure_mono instOuterMeasureClass
measure_mono_left 📖	mathematical	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder	ENNReal ENNReal.instPartialOrder DFunLike.coe Set instFunLike	—	—
measure_support_eq_zero_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Function.support instZeroENNReal Filter.EventuallyEq MeasureTheory.ae instOuterMeasureClass Pi.instZero	—	—
measure_toMeasurable_add_inter_left 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instInter MeasureTheory.toMeasurable instAdd	—	measure_inter_eq_of_measure_eq measure_eq_left_of_subset_of_measure_add_eq MeasureTheory.measure_toMeasurable MeasureTheory.subset_toMeasurable
measure_toMeasurable_add_inter_right 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instInter MeasureTheory.toMeasurable instAdd	—	add_comm measure_toMeasurable_add_inter_left
measure_toMeasurable_inter 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.instInter MeasureTheory.toMeasurable	—	measure_inter_eq_of_measure_eq MeasureTheory.measure_toMeasurable MeasureTheory.subset_toMeasurable
measure_univ_eq_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike Set.univ instZeroENNReal instZero	—	bot_unique MeasureTheory.measure_mono instOuterMeasureClass Set.subset_univ
measure_univ_ne_zero 📖	—	—	—	—	Iff.not measure_univ_eq_zero
measure_univ_pos 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal DFunLike.coe MeasureTheory.Measure Set instFunLike Set.univ	—	pos_iff_ne_zero ENNReal.instCanonicallyOrderedAdd measure_univ_ne_zero
mem_cofinite 📖	mathematical	—	Set Filter Filter.instMembership cofinite ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure instFunLike Compl.compl Set.instCompl Top.top instTopENNReal	—	—
nnreal_smul_coe_apply 📖	mathematical	—	NNReal ENNReal Algebra.toSMul instCommSemiringNNReal CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.instAlgebraNNReal Algebra.id DFunLike.coe MeasureTheory.Measure Set instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring ENNReal.ofNNReal	—	—
nonempty_of_neZero 📖	—	—	—	—	isEmpty_or_nonempty Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.measure_empty instOuterMeasureClass instNeZeroENNRealCoeSetUniv
nonpos_iff_eq_zero' 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder instZero	—	LE.le.ge_iff_eq' zero_le
sInf_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike InfSet.sInf instInfSet MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instFunLikeSetENNReal ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasureTheory.OuterMeasure.instCompleteLattice Set.image toOuterMeasure	—	MeasureTheory.toMeasure_apply sInf_caratheodory
sInf_caratheodory 📖	mathematical	MeasurableSet	MeasureTheory.OuterMeasure.caratheodory InfSet.sInf MeasureTheory.OuterMeasure ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice MeasureTheory.OuterMeasure.instCompleteLattice Set.image MeasureTheory.Measure toOuterMeasure	—	MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen MeasureTheory.OuterMeasure.boundedBy_caratheodory MeasureTheory.measure_eq_iInf MeasureTheory.OuterMeasure.sInfGen_def iInf_image iInf₂_le_of_le MeasureTheory.measure_mono MeasureTheory.OuterMeasure.instOuterMeasureClass MeasureTheory.measure_inter_add_diff add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Set.inter_subset_inter_left Set.diff_subset_diff_left
smul_apply 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike instSMul	—	—
smul_toOuterMeasure 📖	mathematical	—	toOuterMeasure MeasureTheory.Measure instSMul MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instSMul	—	—
sum_add_sum 📖	mathematical	—	MeasureTheory.Measure instAdd sum	—	ext sum_apply Summable.tsum_add ENNReal.instT2Space ENNReal.instContinuousAdd SummationFilter.instNeBotUnconditional ENNReal.summable
sum_add_sum_compl 📖	mathematical	—	MeasureTheory.Measure instAdd sum Set.Elem Set Set.instMembership Compl.compl Set.instCompl	—	ext sum_apply Summable.tsum_add_tsum_compl ENNReal.instT2Space ENNReal.instContinuousAdd ENNReal.summable
sum_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike sum tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	MeasureTheory.toMeasure_apply
sum_apply_eq_zero 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike sum instZeroENNReal	—	sum_apply_of_countable
sum_apply_eq_zero' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike sum instZeroENNReal	—	sum_apply
sum_apply_of_countable 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike sum tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	le_antisymm MeasureTheory.exists_measurable_superset_forall_eq MeasureTheory.measure_mono instOuterMeasureClass sum_apply le_sum_apply
sum_apply₀ 📖	mathematical	MeasureTheory.NullMeasurableSet sum	DFunLike.coe MeasureTheory.Measure Set ENNReal instFunLike tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	le_antisymm instOuterMeasureClass MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq MeasureTheory.measure_congr Filter.EventuallyEq.symm sum_apply ENNReal.tsum_le_tsum MeasureTheory.measure_mono le_sum_apply
sum_bool 📖	mathematical	—	sum MeasureTheory.Measure instAdd	—	sum_fintype Fintype.sum_bool
sum_coe_finset 📖	mathematical	—	sum Finset SetLike.instMembership Finset.instSetLike Finset.sum MeasureTheory.Measure instAddCommMonoid	—	sum_fintype Finset.sum_coe_sort
sum_comm 📖	mathematical	—	sum	—	ext sum_apply ENNReal.tsum_comm
sum_comp_equiv 📖	mathematical	—	sum MeasureTheory.Measure DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike	—	ext sum_apply Equiv.tsum_eq
sum_cond 📖	mathematical	—	sum MeasureTheory.Measure instAdd	—	sum_bool
sum_congr 📖	mathematical	—	sum	—	—
sum_eq_zero 📖	mathematical	—	sum MeasureTheory.Measure instZero	—	sum_apply forall_swap
sum_extend_zero 📖	mathematical	—	sum Function.extend MeasureTheory.Measure Pi.instZero instZero	—	ext sum_apply Function.apply_extend tsum_extend_zero
sum_fintype 📖	mathematical	—	sum Finset.sum MeasureTheory.Measure instAddCommMonoid Finset.univ	—	ext sum_apply tsum_fintype SummationFilter.instLeAtTopUnconditional finset_sum_apply
sum_of_isEmpty 📖	mathematical	—	sum MeasureTheory.Measure instZero	—	measure_univ_eq_zero sum_apply MeasurableSet.univ tsum_empty
sum_sum 📖	mathematical	—	sum	—	ext sum_apply ENNReal.tsum_prod'
sum_zero 📖	mathematical	—	sum MeasureTheory.Measure instZero	—	ext sum_apply tsum_zero
toOuterMeasure_le 📖	mathematical	—	MeasureTheory.OuterMeasure Preorder.toLE PartialOrder.toPreorder MeasureTheory.OuterMeasure.instPartialOrder toOuterMeasure MeasureTheory.Measure instPartialOrder	—	—
toOuterMeasure_top 📖	mathematical	—	toOuterMeasure Top.top MeasureTheory.Measure OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instCompleteLattice	—	—
top_add 📖	mathematical	—	MeasureTheory.Measure instAdd Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique le_add_right le_rfl
zero_le 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder instPartialOrder instZero	—	bot_le
zero_toOuterMeasure 📖	mathematical	—	toOuterMeasure MeasureTheory.Measure instZero MeasureTheory.OuterMeasure MeasureTheory.OuterMeasure.instZero	—	—

MeasureTheory.Measure.ae

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
neBot 📖	mathematical	—	Filter.NeBot MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_neBot

MeasureTheory.Measure.cofinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsMeasurablyGenerated 📖	mathematical	—	Filter.IsMeasurablyGenerated MeasureTheory.Measure.cofinite	—	MeasureTheory.Measure.compl_mem_cofinite MeasureTheory.measure_toMeasurable MeasurableSet.compl MeasureTheory.measurableSet_toMeasurable Set.compl_subset_comm MeasureTheory.subset_toMeasurable

MeasureTheory.OuterMeasure

Definitions

Name	Category	Theorems
toMeasure 📖	CompOp	8 math math: MeasureTheory.toOuterMeasure_toMeasure, MeasureTheory.toMeasure_toOuterMeasure, MeasureTheory.le_toMeasure_apply, MeasureTheory.Measure.pi_def, MeasureTheory.toMeasure_apply, toMeasure_zero, toMeasure_eq_zero, toMeasure_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toMeasure_eq_zero 📖	mathematical	MeasurableSpace MeasurableSpace.instLE caratheodory	toMeasure MeasureTheory.Measure MeasureTheory.Measure.instZero MeasureTheory.OuterMeasure instZero	—	ext le_bot_iff LE.le.trans_eq MeasureTheory.le_toMeasure_apply toMeasure_zero
toMeasure_top 📖	mathematical	—	toMeasure Top.top MeasureTheory.OuterMeasure OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder MeasureTheory.Measure MeasureTheory.Measure.instCompleteLattice	—	MeasureTheory.toOuterMeasure_toMeasure
toMeasure_zero 📖	mathematical	MeasurableSpace MeasurableSpace.instLE caratheodory MeasureTheory.OuterMeasure instZero	toMeasure MeasureTheory.Measure MeasureTheory.Measure.instZero	—	MeasureTheory.Measure.ext MeasureTheory.toMeasure_apply

Monotone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
measure_iInter 📖	mathematical	Monotone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra MeasureTheory.NullMeasurableSet	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iInter iInf ConditionallyCompletePartialOrderInf.toInfSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderInf ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	le_antisymm le_iInf MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.iInter_subset Filter.exists_seq_antitone_tendsto_atTop_atBot le_iInf_comp Directed.measure_iInter instCountableNat Antitone.directed_ge instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat comp_antitone Filter.Eventually.exists Filter.atTop_neBot Filter.Tendsto.eventually_le_atBot ne_top_of_le_ne_top Set.iInter_mono'
measure_iUnion 📖	mathematical	Monotone Set PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike Set.iUnion iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder	—	isEmpty_or_nonempty Set.iUnion_of_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ciSup_of_empty bot_eq_zero' ENNReal.instCanonicallyOrderedAdd Filter.exists_seq_monotone_tendsto_atTop_atTop iUnion_comp_tendsto_atTop Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat iSup_comp_tendsto_atTop MeasureTheory.measure_mono Directed.measure_iUnion instCountableNat directed_le comp

---

← Back to Index