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

• Set.Accumulate s x = ⋃ (y : α), ⋃ (_ : y ≤ x), s y

theorem Set.accumulate_def {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} : Set.Accumulate s x = ⋃ (y : α), ⋃ (_ : y ≤ x), s y

@[simp]

theorem Set.mem_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [LE α] {x : α} {z : β} : z ∈ Set.Accumulate s x ↔ ∃ y ≤ x, z ∈ s y

theorem Set.subset_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] {x : α} : s x ⊆ Set.Accumulate s x

theorem Set.accumulate_subset_iUnion {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] (x : α) : Set.Accumulate s x ⊆ ⋃ (i : α), s i

theorem Set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : Monotone (Set.Accumulate s)

theorem Set.biUnion_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] (x : α) : ⋃ (y : α), ⋃ (_ : y ≤ x), Set.Accumulate s y = ⋃ (y : α), ⋃ (_ : y ≤ x), s y

theorem Set.iUnion_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] : ⋃ (x : α), Set.Accumulate s x = ⋃ (x : α), s x