Exhaustion

📁 Source: Mathlib/MeasureTheory/Measure/Decomposition/Exhaustion.lean

Statistics

Metric	Count
Definitions sigmaFiniteSet, sigmaFiniteSetGE, sigmaFiniteSetWRT, sigmaFiniteSetWRT'	4
Theorems exists_isSigmaFiniteSet_measure_ge, instSigmaFiniteRestrictSigmaFiniteSet, instSigmaFiniteRestrictSigmaFiniteSetWRT, measurableSet_sigmaFiniteSet, measurableSet_sigmaFiniteSetGE, measurableSet_sigmaFiniteSetWRT, measurableSet_sigmaFiniteSetWRT', measure_compl_sigmaFiniteSet, measure_compl_sigmaFiniteSetWRT, measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT', measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet, measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet, measure_sigmaFiniteSetGE_ge, measure_sigmaFiniteSetGE_le, measure_sigmaFiniteSetWRT', restrict_compl_sigmaFiniteSetWRT, restrict_compl_sigmaFiniteSet_eq_zero_or_top, sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero, sigmaFinite_restrict_sigmaFiniteSetGE, sigmaFinite_restrict_sigmaFiniteSetWRT', tendsto_measure_sigmaFiniteSetGE	23
Total	27

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_isSigmaFiniteSet_measure_ge 📖	mathematical	—	MeasurableSet SigmaFinite Measure.restrict ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub iSup Set ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder DFunLike.coe Measure Measure.instFunLike DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddMonoidWithOne.toNatCast	—	LE.le.trans_lt iSup_le measure_mono Measure.instOuterMeasureClass Set.subset_univ measure_lt_top exists_lt_of_lt_ciSup ENNReal.sub_lt_self LT.lt.ne LT.lt.ne_bot one_div iSup_neg bot_eq_zero' ENNReal.instCanonicallyOrderedAdd iSup_congr_Prop ENNReal.iSup_zero LT.lt.le iSup_true MeasurableSet.empty Measure.restrict_empty IsFiniteMeasure.toSigmaFinite isFiniteMeasureZero tsub_eq_zero_of_le ENNReal.instOrderedSub zero_le
instSigmaFiniteRestrictSigmaFiniteSet 📖	mathematical	—	SigmaFinite Measure.restrict Measure.sigmaFiniteSet	—	Measure.sigmaFiniteSet.eq_1 instSigmaFiniteRestrictSigmaFiniteSetWRT
instSigmaFiniteRestrictSigmaFiniteSetWRT 📖	mathematical	—	SigmaFinite Measure.restrict Measure.sigmaFiniteSetWRT	—	Measure.sigmaFiniteSetWRT.eq_1 Measure.restrict_empty IsFiniteMeasure.toSigmaFinite isFiniteMeasureZero
measurableSet_sigmaFiniteSet 📖	mathematical	—	MeasurableSet Measure.sigmaFiniteSet	—	measurableSet_sigmaFiniteSetWRT
measurableSet_sigmaFiniteSetGE 📖	mathematical	—	MeasurableSet Measure.sigmaFiniteSetGE	—	exists_isSigmaFiniteSet_measure_ge
measurableSet_sigmaFiniteSetWRT 📖	mathematical	—	MeasurableSet Measure.sigmaFiniteSetWRT	—	Measure.sigmaFiniteSetWRT.eq_1 MeasurableSet.empty
measurableSet_sigmaFiniteSetWRT' 📖	mathematical	—	MeasurableSet Measure.sigmaFiniteSetWRT'	—	MeasurableSet.iUnion instCountableNat measurableSet_sigmaFiniteSetGE
measure_compl_sigmaFiniteSet 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl Measure.sigmaFiniteSet instZeroENNReal	—	measure_compl_sigmaFiniteSetWRT Measure.AbsolutelyContinuous.rfl instSFiniteOfSigmaFinite
measure_compl_sigmaFiniteSetWRT 📖	mathematical	Measure.AbsolutelyContinuous	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl Measure.sigmaFiniteSetWRT instZeroENNReal	—	measure_eq_top_of_subset_compl_sigmaFiniteSetWRT subset_rfl Set.instReflSubset ENNReal.top_ne_zero Measure.iSup_restrict_spanningSets Measure.restrict_apply' measurableSet_spanningSets Set.inter_subset_left ne_of_lt LE.le.trans_lt measure_mono Measure.instOuterMeasureClass Set.inter_subset_right measure_spanningSets_lt_top
measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl Measure.sigmaFiniteSet instZeroENNReal SigmaFinite	—	sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero measure_compl_sigmaFiniteSet
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl Measure.sigmaFiniteSetWRT	DFunLike.coe Measure ENNReal Measure.instFunLike Top.top instTopENNReal	—	exists_isFiniteMeasure_absolutelyContinuous measurableSet_sigmaFiniteSetWRT' sigmaFinite_restrict_sigmaFiniteSetWRT' measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' Measure.sigmaFiniteSetWRT.eq_1
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl Measure.sigmaFiniteSetWRT'	DFunLike.coe Measure ENNReal Measure.instFunLike Top.top instTopENNReal	—	measure_eq_iInf measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet measure_mono_null Measure.instOuterMeasureClass Set.subset_inter Set.inter_subset_right MeasurableSet.inter MeasurableSet.compl measurableSet_sigmaFiniteSetWRT' measure_mono_top Set.inter_subset_left
measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet 📖	mathematical	MeasurableSet Set Set.instHasSubset Compl.compl Set.instCompl Measure.sigmaFiniteSetWRT'	DFunLike.coe Measure ENNReal Measure.instFunLike Top.top instTopENNReal	—	measure_union Disjoint.mono_right disjoint_compl_right ENNReal.lt_add_right measure_ne_top measure_sigmaFiniteSetWRT' LE.le.trans le_iSup sigmaFinite_restrict_sigmaFiniteSetWRT' instSigmaFiniteRestrictUnionSet le_iSup₂ MeasurableSet.union measurableSet_sigmaFiniteSetWRT' LT.lt.not_ge Ne.lt_top IsFiniteMeasure.toSigmaFinite Restrict.isFiniteMeasure
measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl Measure.sigmaFiniteSet	DFunLike.coe Measure ENNReal Measure.instFunLike instZeroENNReal Top.top instTopENNReal	—	measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
measure_sigmaFiniteSetGE_ge 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub iSup Set ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasurableSet SigmaFinite Measure.restrict DFunLike.coe Measure Measure.instFunLike DivInvMonoid.toDiv ENNReal.instDivInvMonoid AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal AddMonoidWithOne.toNatCast Measure.sigmaFiniteSetGE	—	exists_isSigmaFiniteSet_measure_ge
measure_sigmaFiniteSetGE_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe Measure Set Measure.instFunLike Measure.sigmaFiniteSetGE iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasurableSet SigmaFinite Measure.restrict	—	LE.le.trans le_iSup sigmaFinite_restrict_sigmaFiniteSetGE le_iSup₂ measurableSet_sigmaFiniteSetGE
measure_sigmaFiniteSetWRT' 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.sigmaFiniteSetWRT' iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasurableSet SigmaFinite Measure.restrict	—	le_antisymm LE.le.trans le_iSup sigmaFinite_restrict_sigmaFiniteSetWRT' le_iSup₂ measurableSet_sigmaFiniteSetWRT' le_of_tendsto' instClosedIicTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat tendsto_measure_sigmaFiniteSetGE measure_mono Measure.instOuterMeasureClass Set.subset_iUnion
restrict_compl_sigmaFiniteSetWRT 📖	mathematical	Measure.AbsolutelyContinuous	Measure.restrict Compl.compl Set Set.instCompl Measure.sigmaFiniteSetWRT ENNReal Measure Measure.instSMul Algebra.toSMul ENNReal.instCommSemiring CommSemiring.toSemiring Algebra.id IsScalarTower.right Top.top instTopENNReal	—	Measure.ext IsScalarTower.right Measure.restrict_apply' MeasurableSet.compl measurableSet_sigmaFiniteSetWRT Measure.smul_apply smul_eq_mul MulZeroClass.mul_zero ENNReal.top_mul measure_eq_top_of_subset_compl_sigmaFiniteSetWRT Set.inter_subset_right
restrict_compl_sigmaFiniteSet_eq_zero_or_top 📖	mathematical	—	DFunLike.coe Measure Set ENNReal Measure.instFunLike Measure.restrict Compl.compl Set.instCompl Measure.sigmaFiniteSet instZeroENNReal Top.top instTopENNReal	—	Measure.restrict_apply' MeasurableSet.compl measurableSet_sigmaFiniteSet measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right
sigmaFinite_of_measure_compl_sigmaFiniteSet_eq_zero 📖	mathematical	DFunLike.coe Measure Set ENNReal Measure.instFunLike Compl.compl Set.instCompl Measure.sigmaFiniteSet instZeroENNReal	SigmaFinite	—	Measure.restrict_add_restrict_compl measurableSet_sigmaFiniteSet Measure.restrict_eq_zero add_zero instSigmaFiniteRestrictSigmaFiniteSet
sigmaFinite_restrict_sigmaFiniteSetGE 📖	mathematical	—	SigmaFinite Measure.restrict Measure.sigmaFiniteSetGE	—	exists_isSigmaFiniteSet_measure_ge
sigmaFinite_restrict_sigmaFiniteSetWRT' 📖	mathematical	—	SigmaFinite Measure.restrict Measure.sigmaFiniteSetWRT'	—	sigmaFinite_restrict_sigmaFiniteSetGE Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT' Set.compl_inter_self measure_empty Measure.instOuterMeasureClass LE.le.trans_lt measure_mono Set.inter_subset_left measurableSet_sigmaFiniteSetGE measure_spanningSets_lt_top Set.union_iUnion Set.iUnion_unpair Set.iUnion_congr Set.iUnion_inter iUnion_spanningSets Set.univ_inter Set.compl_union_self Measure.FiniteSpanningSetsIn.sigmaFinite
tendsto_measure_sigmaFiniteSetGE 📖	mathematical	—	Filter.Tendsto ENNReal DFunLike.coe Measure Set Measure.instFunLike Measure.sigmaFiniteSetGE Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot ENNReal.instCompleteLinearOrder MeasurableSet SigmaFinite Measure.restrict	—	tendsto_of_tendsto_of_tendsto_of_le_of_le ENNReal.instOrderTopology tsub_zero ENNReal.instOrderedSub ENNReal.Tendsto.sub tendsto_const_nhds one_div ENNReal.tendsto_inv_nat_nhds_zero ENNReal.zero_ne_top measure_sigmaFiniteSetGE_ge measure_sigmaFiniteSetGE_le

MeasureTheory.Measure

Definitions

Name	Category	Theorems
sigmaFiniteSet 📖	CompOp	6 math math: MeasureTheory.measure_compl_sigmaFiniteSet, MeasureTheory.restrict_compl_sigmaFiniteSet, MeasureTheory.measurableSet_sigmaFiniteSet, MeasureTheory.measure_compl_sigmaFiniteSet_eq_zero_iff_sigmaFinite, MeasureTheory.restrict_compl_sigmaFiniteSet_eq_zero_or_top, MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSet
sigmaFiniteSetGE 📖	CompOp	5 math math: MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.measure_sigmaFiniteSetGE_le, MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, MeasureTheory.measure_sigmaFiniteSetGE_ge
sigmaFiniteSetWRT 📖	CompOp	4 math math: MeasureTheory.measure_compl_sigmaFiniteSetWRT, MeasureTheory.instSigmaFiniteRestrictSigmaFiniteSetWRT, MeasureTheory.restrict_compl_sigmaFiniteSetWRT, MeasureTheory.measurableSet_sigmaFiniteSetWRT
sigmaFiniteSetWRT' 📖	CompOp	3 math math: MeasureTheory.measure_sigmaFiniteSetWRT', MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT'

---

← Back to Index