AddContent

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

Statistics

Metric	Count
Definitions IsSigmaSubadditive, extend, onIoc, onIocAux, supClosure, toFun, addContent_of_union, instFunLikeAddContentSet, instInhabitedAddContent	9
Theorems empty', ext, ext_iff, extend_eq, extend_eq_extend, extend_eq_top, onIocAux_apply, onIocAux_empty, onIoc_apply, sUnion', supClosure_apply, supClosure_apply_finpartition, supClosure_apply_of_mem, addContent_accumulate, addContent_biUnion, addContent_biUnion_eq, addContent_biUnion_le, addContent_diff_of_ne_top, addContent_empty, addContent_eq_add_disjointOfDiffUnion_of_subset, addContent_iUnion, addContent_iUnion_eq_sum_of_tendsto_zero, addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive, addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le, addContent_le_sum_of_subset_sUnion, addContent_mono, addContent_sUnion, addContent_sUnion_le_sum, addContent_union, addContent_union', addContent_union_le, eq_add_disjointOfDiff_of_subset, isSigmaSubadditive_of_addContent_iUnion_eq_tsum, le_addContent_diff, sum_addContent_eq_of_sUnion_eq, sum_addContent_le_of_subset, tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum	37
Total	46

MeasureTheory

Definitions

Name	Category	Theorems
instFunLikeAddContentSet 📖	CompOp	49 math math: sum_addContent_le_of_subset, piContent_tendsto_zero, ProbabilityTheory.Kernel.trajContent_cylinder, AddContent.measure_eq, piContent_cylinder, addContent_diff_of_ne_top, AddContent.extend_eq, projectiveFamilyContent_eq, projectiveFamilyContent_diff, AddContent.isCaratheodory_inducedOuterMeasure_of_mem, ProbabilityTheory.Kernel.trajContent_tendsto_zero, AddContent.supClosure_apply_finpartition, projectiveFamilyContent_cylinder, projectiveFamilyContent_congr, piContent_eq_measure_pi, addContent_sUnion, sum_addContent_eq_of_sUnion_eq, Measure.infinitePiNat_map_piCongrLeft, addContent_mono, addContent_union', projectiveFamilyContent_diff_of_subset, addContent_union, addContent_biUnion_eq, AddContent.inducedOuterMeasure_eq, AddContent.isCaratheodory_inducedOuterMeasure, addContent_eq_add_disjointOfDiffUnion_of_subset, AddContent.ext_iff, addContent_biUnion, addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive, projectiveFamilyContent_iUnion_le, AddContent.extend_eq_top, addContent_sUnion_le_sum, addContent_accumulate, AddContent.supClosure_apply_of_mem, AddContent.measureCaratheodory_eq_inducedOuterMeasure, addContent_iUnion, addContent_biUnion_le, ProbabilityTheory.Kernel.trajContent_eq_lmarginalPartialTraj, le_addContent_diff, AddContent.onIoc_apply, projectiveFamilyContent_mono, AddContent.supClosure_apply, eq_add_disjointOfDiff_of_subset, addContent_empty, addContent_le_sum_of_subset_sUnion, AddContent.extend_eq_extend, Measure.piContent_eq_infinitePiNat, addContent_union_le, AddContent.measureCaratheodory_eq
instInhabitedAddContent 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
addContent_accumulate 📖	mathematical	IsSetRing Pairwise Function.onFun Set Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership	DFunLike.coe AddContent instFunLikeAddContentSet Set.accumulate Finset.sum Finset.range	—	Set.accumulate_zero_nat Finset.sum_congr zero_add Finset.sum_singleton Finset.sum_range_succ Set.accumulate_succ addContent_union IsSetRing.accumulate_mem Set.disjoint_accumulate
addContent_biUnion 📖	mathematical	Set Set.instMembership Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset Finset.instSetLike Set.iUnion Finset.instMembership	DFunLike.coe AddContent instFunLikeAddContentSet Finset.sum	—	Finset.coe_image Set.sUnion_image Set.iUnion_congr_Prop addContent_sUnion Set.Pairwise.image Finset.sum_image_of_pairwise_eq_zero Set.Pairwise.imp
addContent_biUnion_eq 📖	mathematical	IsSetRing Set Set.instMembership Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice SetLike.coe Finset Finset.instSetLike	DFunLike.coe AddContent instFunLikeAddContentSet Set.iUnion Finset.instMembership Finset.sum	—	Finset.induction Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty addContent_empty Finset.sum_insert Finset.coe_insert Set.biUnion_insert addContent_union IsSetRing.biUnion_mem Set.disjoint_iUnion₂_right
addContent_biUnion_le 📖	mathematical	IsSetRing Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddContent instFunLikeAddContentSet Set.iUnion Finset Finset.instMembership Finset.sum	—	Finset.induction Set.iUnion_congr_Prop Set.iUnion_of_empty instIsEmptyFalse Set.iUnion_empty addContent_empty Finset.sum_insert Finset.coe_insert Set.biUnion_insert LE.le.trans addContent_union_le IsSetRing.biUnion_mem add_le_add CanonicallyOrderedAdd.toAddLeftMono covariant_swap_add_of_covariant_add le_rfl
addContent_diff_of_ne_top 📖	mathematical	IsSetRing Set Set.instMembership Set.instHasSubset	DFunLike.coe AddContent ENNReal ENNReal.instAddCommMonoid instFunLikeAddContentSet Set.instSDiff ENNReal.instSub	—	addContent_union IsSetRing.diff_mem disjoint_sdiff_self_right Set.union_eq_right Set.union_diff_self ENNReal.add_sub_cancel_left
addContent_empty 📖	mathematical	—	DFunLike.coe AddContent Set instFunLikeAddContentSet Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	AddContent.empty'
addContent_eq_add_disjointOfDiffUnion_of_subset 📖	mathematical	IsSetSemiring Set Set.instMembership Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe AddContent instFunLikeAddContentSet AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.sum IsSetSemiring.disjointOfDiffUnion	—	IsSetSemiring.sUnion_union_disjointOfDiffUnion_of_subset addContent_sUnion Finset.coe_union Set.union_subset IsSetSemiring.disjointOfDiffUnion_subset IsSetSemiring.pairwiseDisjoint_union_disjointOfDiffUnion Finset.sum_union IsSetSemiring.disjoint_disjointOfDiffUnion
addContent_iUnion 📖	mathematical	Set Set.instMembership Pairwise Function.onFun Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.iUnion	DFunLike.coe AddContent instFunLikeAddContentSet Finset.sum Finset.univ	—	Set.iUnion_congr_Prop Set.iUnion_true addContent_biUnion Finset.coe_univ
addContent_iUnion_eq_sum_of_tendsto_zero 📖	mathematical	IsSetRing Filter.Tendsto ENNReal DFunLike.coe AddContent ENNReal.instAddCommMonoid Set instFunLikeAddContentSet Filter.atTop Nat.instPreorder nhds ENNReal.instTopologicalSpace instZeroENNReal Set.instMembership Set.iUnion Pairwise Function.onFun Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	tsum SummationFilter.unconditional	—	IsSetRing.diff_mem IsSetRing.accumulate_mem Set.mem_diff Set.monotone_accumulate Set.iInter_inter_distrib Set.iInter_const Set.compl_iUnion Set.iUnion_accumulate Set.inter_compl_self addContent_diff_of_ne_top Set.accumulate_subset_iUnion addContent_accumulate tendsto_nhds_unique ENNReal.instT2Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.tendsto_add_atTop_iff_nat ENNReal.tendsto_const_sub_nhds_zero_iff addContent_mono ENNReal.instCanonicallyOrderedAdd IsSetRing.isSetSemiring ENNReal.tendsto_nat_tsum
addContent_iUnion_eq_tsum_of_disjoint_of_IsSigmaSubadditive 📖	mathematical	IsSetSemiring AddContent.IsSigmaSubadditive Set Set.instMembership Set.iUnion Pairwise Function.onFun Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe AddContent ENNReal ENNReal.instAddCommMonoid instFunLikeAddContentSet tsum ENNReal.instTopologicalSpace SummationFilter.unconditional	—	addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le
addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le 📖	—	IsSetSemiring ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe AddContent ENNReal.instAddCommMonoid Set instFunLikeAddContentSet Set.iUnion tsum ENNReal.instTopologicalSpace SummationFilter.unconditional Set.instMembership Pairwise Function.onFun Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	—	le_antisymm Summable.tsum_le_of_sum_le OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology SummationFilter.instNeBotUnconditional ENNReal.summable Finset.sum_image_of_disjoint addContent_empty Pairwise.pairwiseDisjoint sum_addContent_le_of_subset ENNReal.instCanonicallyOrderedAdd Finset.coe_image HasSubset.Subset.trans Set.instIsTransSubset Set.subset_preimage_image Set.preimage_mono Set.mem_image Set.subset_iUnion
addContent_le_sum_of_subset_sUnion 📖	mathematical	IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.instMembership Set.sUnion	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddContent instFunLikeAddContentSet Finset.sum	—	Finset.coe_image Set.sUnion_image Set.inter_iUnion₂ Set.inter_eq_self_of_subset_left Set.sUnion_eq_biUnion LE.le.trans addContent_sUnion_le_sum IsSetSemiring.inter_mem Finset.sum_image_le_of_nonneg CanonicallyOrderedAdd.toAddLeftMono zero_le Finset.sum_le_sum addContent_mono Set.inter_subset_right
addContent_mono 📖	mathematical	IsSetSemiring Set Set.instMembership Set.instHasSubset	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddContent instFunLikeAddContentSet	—	sum_addContent_le_of_subset Finset.singleton_subset_set_iff Finset.coe_singleton Finset.sum_singleton
addContent_sUnion 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership Set.sUnion	DFunLike.coe AddContent instFunLikeAddContentSet Finset.sum	—	AddContent.sUnion'
addContent_sUnion_le_sum 📖	mathematical	IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.instMembership Set.sUnion	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddContent instFunLikeAddContentSet Finset.sum	—	IsSetSemiring.pairwiseDisjoint_disjointOfUnion Finset.disjiUnion_eq_biUnion Finset.coe_biUnion Set.iUnion_congr_Prop IsSetSemiring.disjointOfUnion_subset IsSetSemiring.pairwiseDisjoint_biUnion_disjointOfUnion IsSetSemiring.disjointOfUnion_props addContent_sUnion Finset.sum_disjiUnion Finset.sum_le_sum CanonicallyOrderedAdd.toAddLeftMono sum_addContent_le_of_subset IsSetSemiring.pairwiseDisjoint_disjointOfUnion_of_mem IsSetSemiring.subset_of_mem_disjointOfUnion
addContent_union 📖	mathematical	IsSetRing Set Set.instMembership Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe AddContent instFunLikeAddContentSet Set.instUnion AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	addContent_union' IsSetRing.union_mem
addContent_union' 📖	mathematical	Set Set.instMembership Set.instUnion Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe AddContent instFunLikeAddContentSet AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.ext Matrix.cons_val_fin_one Finset.sum_congr Fin.univ_castSuccEmb Finset.univ_unique Finset.map_singleton Finset.cons.congr_simp Finset.cons_eq_insert Finset.sum_insert Fin.instNeZeroHAddNatOfNat_mathlib_1 Finset.sum_singleton add_comm addContent_iUnion Fintype.complete
addContent_union_le 📖	mathematical	IsSetRing Set Set.instMembership	Preorder.toLE PartialOrder.toPreorder DFunLike.coe AddContent instFunLikeAddContentSet Set.instUnion AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	Set.union_diff_self addContent_union IsSetRing.diff_mem Set.disjoint_iff_inter_eq_empty Set.inter_diff_self add_le_add_right CanonicallyOrderedAdd.toAddLeftMono addContent_mono IsSetRing.isSetSemiring Set.diff_subset
eq_add_disjointOfDiff_of_subset 📖	mathematical	IsSetSemiring Set Set.instMembership Set.instHasSubset	DFunLike.coe AddContent instFunLikeAddContentSet AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Finset.sum IsSetSemiring.disjointOfDiff	—	IsSetSemiring.sUnion_insert_disjointOfDiff Finset.coe_insert addContent_sUnion Set.insert_subset IsSetSemiring.subset_disjointOfDiff IsSetSemiring.pairwiseDisjoint_insert_disjointOfDiff Finset.sum_insert IsSetSemiring.notMem_disjointOfDiff
isSigmaSubadditive_of_addContent_iUnion_eq_tsum 📖	mathematical	IsSetRing DFunLike.coe AddContent ENNReal ENNReal.instAddCommMonoid Set instFunLikeAddContentSet Set.iUnion tsum ENNReal.instTopologicalSpace SummationFilter.unconditional	AddContent.IsSigmaSubadditive	—	Set.iSup_eq_iUnion iSup_partialSups_eq tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum partialSups_monotone IsSetRing.partialSups_mem Filter.tendsto_add_atTop_iff_nat ENNReal.tendsto_nat_tsum le_of_tendsto_of_tendsto' OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat partialSups_eq_biUnion_range addContent_biUnion_le ENNReal.instCanonicallyOrderedAdd
le_addContent_diff 📖	mathematical	IsSetRing Set Set.instMembership	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ENNReal.instSub DFunLike.coe AddContent ENNReal.instAddCommMonoid instFunLikeAddContentSet Set.instSDiff	—	Set.inter_union_diff addContent_union IsSetRing.inter_mem IsSetRing.diff_mem disjoint_inf_sdiff add_comm LE.le.trans_eq add_tsub_le_assoc ENNReal.instOrderedSub IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid tsub_eq_zero_of_le ENNReal.instCanonicallyOrderedAdd addContent_mono IsSetRing.isSetSemiring Set.inter_subset_right add_zero
sum_addContent_eq_of_sUnion_eq 📖	mathematical	IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.sUnion	Finset.sum DFunLike.coe AddContent instFunLikeAddContentSet	—	Finset.sum_congr Set.subset_sUnion_of_mem addContent_biUnion IsSetSemiring.inter_mem Set.PairwiseDisjoint.mono Finset.sum_comm
sum_addContent_le_of_subset 📖	mathematical	IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership	Preorder.toLE PartialOrder.toPreorder Finset.sum DFunLike.coe AddContent instFunLikeAddContentSet	—	addContent_eq_add_disjointOfDiffUnion_of_subset le_add_right le_rfl
tendsto_atTop_addContent_iUnion_of_addContent_iUnion_eq_tsum 📖	mathematical	IsSetRing DFunLike.coe AddContent ENNReal ENNReal.instAddCommMonoid Set instFunLikeAddContentSet Set.iUnion tsum ENNReal.instTopologicalSpace SummationFilter.unconditional Monotone Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.instMembership	Filter.Tendsto Filter.atTop nhds	—	iUnion_disjointed IsSetRing.disjointed_mem disjoint_disjointed addContent_accumulate Monotone.partialSups_eq partialSups_disjointed partialSups_eq_biSup Set.accumulate.eq_1 Filter.tendsto_add_atTop_iff_nat ENNReal.tendsto_nat_tsum

MeasureTheory.AddContent

Definitions

Name	Category	Theorems
IsSigmaSubadditive 📖	MathDef	3 math math: ProbabilityTheory.Kernel.isSigmaSubadditive_trajContent, MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum, MeasureTheory.isSigmaSubadditive_piContent
extend 📖	CompOp	3 math math: extend_eq, extend_eq_top, extend_eq_extend
onIoc 📖	CompOp	1 math math: onIoc_apply
onIocAux 📖	CompOp	2 math math: onIocAux_apply, onIocAux_empty
supClosure 📖	CompOp	3 math math: supClosure_apply_finpartition, supClosure_apply_of_mem, supClosure_apply
toFun 📖	CompOp	2 math math: sUnion', empty'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
empty' 📖	mathematical	—	toFun Set Set.instEmptyCollection AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	—
ext 📖	—	DFunLike.coe MeasureTheory.AddContent Set MeasureTheory.instFunLikeAddContentSet	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe MeasureTheory.AddContent Set MeasureTheory.instFunLikeAddContentSet	—	ext
extend_eq 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet extend	—	extend_eq_extend MeasureTheory.extend_eq
extend_eq_extend 📖	mathematical	MeasureTheory.IsSetSemiring	DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid Set MeasureTheory.instFunLikeAddContentSet extend MeasureTheory.extend Set.instMembership	—	—
extend_eq_top 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	DFunLike.coe MeasureTheory.AddContent ENNReal ENNReal.instAddCommMonoid MeasureTheory.instFunLikeAddContentSet extend Top.top instTopENNReal	—	extend_eq_extend MeasureTheory.extend_eq_top
onIocAux_apply 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	onIocAux Set.Ioc SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	LE.le.eq_or_lt Set.Ioc_eq_Ioc_iff
onIocAux_empty 📖	mathematical	—	onIocAux Set Set.instEmptyCollection NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	onIocAux.eq_1
onIoc_apply 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder	DFunLike.coe MeasureTheory.AddContent AddCommGroup.toAddCommMonoid setOf Set Set.Ioc MeasureTheory.instFunLikeAddContentSet onIoc SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	onIocAux_apply
sUnion' 📖	mathematical	Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.instMembership Set.sUnion	toFun Finset.sum	—	—
supClosure_apply 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Set.PairwiseDisjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Set.sUnion	DFunLike.coe MeasureTheory.AddContent ClosureOperator PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice ClosureOperator.instFunLike supClosure Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice MeasureTheory.instFunLikeAddContentSet supClosure Finset.sum	—	—
supClosure_apply_finpartition 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finpartition.parts ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	DFunLike.coe MeasureTheory.AddContent ClosureOperator PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder ClosureOperator.instFunLike supClosure Lattice.toSemilatticeSup MeasureTheory.instFunLikeAddContentSet supClosure Finset.sum	—	supClosure_apply Finpartition.disjoint Finpartition.sup_parts Finset.sup_set_eq_biUnion Set.sUnion_eq_biUnion Set.iUnion_congr_Prop
supClosure_apply_of_mem 📖	mathematical	MeasureTheory.IsSetSemiring Set Set.instMembership	DFunLike.coe MeasureTheory.AddContent ClosureOperator PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra ClosureOperator.instFunLike supClosure Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice MeasureTheory.instFunLikeAddContentSet supClosure	—	—

MeasureTheory.IsSetRing

Definitions

Name	Category	Theorems
addContent_of_union 📖	CompOp	—

---

← Back to Index