Theorems · Definition · order theory
Set.accumulate
{α : Type u_1} → {β : Type u_2} → [LE α] → (α → Set β) → α → Set βaccumulate s is the union of s y for y ≤ x.
- Defined in
- Mathlib.Order.SetAccumulate
- Cited by
- 32 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- LE
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Set.iUnionproof · cited by 2,483
Cited by34
Results whose statement or proof uses this declaration.
- MeasureTheory.spanningSetsproof · cited by 45
- compactCoveringproof · cited by 14
- Set.monotone_accumulatestatement · cited by 10
- Set.iUnion_accumulatestatement · cited by 7
- MeasureTheory.tendsto_measure_iUnion_accumulatestatement and proof · cited by 4
- MeasureTheory.IsSetRing.accumulate_memstatement and proof · cited by 4
- Set.accumulate_succstatement · cited by 3
- Set.accumulate_zero_natstatement · cited by 3
- MeasureTheory.addContent_accumulatestatement and proof · cited by 3
- Set.subset_accumulatestatement · cited by 3
- MeasureTheory.exists_measure_symmDiff_lt_of_generateFrom_isSetRingproof · cited by 2
- MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zeroproof · cited by 2