Accumulate

📁 Source: Mathlib/Data/Set/Accumulate.lean

Statistics

Metric	Count
Definitions Accumulate, accumulate	2
Theorems accumulate_bot, accumulate_def, accumulate_subset_accumulate, accumulate_subset_iUnion, accumulate_succ, accumulate_zero_nat, biUnion_accumulate, disjoint_accumulate, iUnion_accumulate, mem_accumulate, monotone_accumulate, partialSups_eq_accumulate, subset_accumulate	13
Total	15

Set

Definitions

Name	Category	Theorems
Accumulate 📖	CompOp	—
accumulate 📖	CompOp	21 math math: accumulate_bot, accumulate_succ, MeasureTheory.FiniteMeasure.tendsto_measure_iUnion_accumulate, disjoint_accumulate, accumulate_subset_accumulate, monotone_accumulate, MeasureTheory.ProbabilityMeasure.tendsto_measure_iUnion_accumulate, iUnion_accumulate, accumulate_def, mem_accumulate, partialSups_eq_accumulate, accumulate_zero_nat, biUnion_accumulate, MeasureTheory.addContent_accumulate, accumulate_subset_iUnion, MeasureTheory.IsSetRing.accumulate_mem, MeasureTheory.tendsto_measure_iUnion_accumulate, subset_accumulate, MeasureTheory.measure_iUnion_eq_iSup_accumulate, isCompact_accumulate, isLindelof_accumulate

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
accumulate_bot 📖	mathematical	—	accumulate Preorder.toLE PartialOrder.toPreorder Bot.bot OrderBot.toBot	—	iUnion_congr_Prop iUnion_iUnion_eq_left
accumulate_def 📖	mathematical	—	accumulate iUnion	—	—
accumulate_subset_accumulate 📖	mathematical	Preorder.toLE	Set instHasSubset accumulate	—	monotone_accumulate
accumulate_subset_iUnion 📖	mathematical	—	Set instHasSubset accumulate iUnion	—	LE.le.trans_eq biUnion_subset_biUnion_left subset_univ biUnion_univ
accumulate_succ 📖	mathematical	—	accumulate Set instUnion	—	biUnion_le_succ
accumulate_zero_nat 📖	mathematical	—	accumulate	—	iUnion_congr_Prop iUnion_iUnion_eq_left
biUnion_accumulate 📖	mathematical	—	iUnion Preorder.toLE accumulate	—	Subset.antisymm iUnion₂_subset monotone_accumulate iUnion₂_mono subset_accumulate
disjoint_accumulate 📖	mathematical	Pairwise Function.onFun Set Disjoint ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice Preorder.toLT	accumulate Preorder.toLE	—	disjoint_left LT.lt.ne LE.le.trans_lt
iUnion_accumulate 📖	mathematical	—	iUnion accumulate Preorder.toLE	—	Subset.antisymm iUnion_mono subset_accumulate
mem_accumulate 📖	mathematical	—	Set instMembership accumulate	—	—
monotone_accumulate 📖	mathematical	—	Monotone Set PartialOrder.toPreorder ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra accumulate Preorder.toLE	—	biUnion_subset_biUnion_left le_trans
partialSups_eq_accumulate 📖	mathematical	—	DFunLike.coe OrderHom Set Nat.instPreorder PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra instCompleteAtomicBooleanAlgebra OrderHom.instFunLike partialSups LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder accumulate	—	ext partialSups_eq_sup_range Finset.sup_set_eq_biUnion iUnion_congr_Prop
subset_accumulate 📖	mathematical	—	Set instHasSubset accumulate Preorder.toLE	—	mem_biUnion le_rfl

---

← Back to Index