# Accumulate #

The function Accumulate takes a set s and returns ⋃ y ≤ x, s y.

def Set.Accumulate {α : Type u_1} {β : Type u_2} [LE α] (s : αSet β) (x : α) :
Set β

Accumulate s is the union of s y for y ≤ x.

Equations
• = ⋃ (y : α), ⋃ (_ : y x), s y
Instances For
theorem Set.accumulate_def {α : Type u_1} {β : Type u_2} {s : αSet β} [LE α] {x : α} :
= ⋃ (y : α), ⋃ (_ : y x), s y
@[simp]
theorem Set.mem_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [LE α] {x : α} {z : β} :
z yx, z s y
theorem Set.subset_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [] {x : α} :
s x
theorem Set.accumulate_subset_iUnion {α : Type u_1} {β : Type u_2} {s : αSet β} [] (x : α) :
⋃ (i : α), s i
theorem Set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [] :
theorem Set.accumulate_subset_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [] {x : α} {y : α} (h : x y) :
theorem Set.biUnion_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [] (x : α) :
⋃ (y : α), ⋃ (_ : y x), = ⋃ (y : α), ⋃ (_ : y x), s y
theorem Set.iUnion_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [] :
⋃ (x : α), = ⋃ (x : α), s x