Accumulate

The function accumulate takes s : α → Set β with LE α and returns ⋃ y ≤ x, s y. It is related to dissipate s := ⋂ y ≤ x, s y.

accumulate is closely related to the function partialSups, although these two functions have slightly different typeclass assumptions and API. partialSups_eq_accumulate shows that they coincide on ℕ.

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 : α} : accumulate s x = ⋃ (y : α), ⋃ (_ : y ≤ x), s y

theorem Set.accumulate_eq_biInter_lt {β : Type u_2} {s : ℕ → Set β} {n : ℕ} : accumulate s n = ⋃ (k : ℕ), ⋃ (_ : k < n + 1), s k

@[simp]

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

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

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

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

theorem Set.accumulate_subset_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] {x y : α} (h : x ≤ y) : accumulate s x ⊆ accumulate s y

@[simp]

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

@[simp]

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

@[simp]

theorem Set.accumulate_bot {α : Type u_1} {β : Type u_2} [PartialOrder α] [OrderBot α] (s : α → Set β) : accumulate s ⊥ = s ⊥

@[simp]

theorem Set.accumulate_zero_nat {β : Type u_2} (s : ℕ → Set β) : accumulate s 0 = s 0

theorem Set.disjoint_accumulate {α : Type u_1} {β : Type u_2} {s : α → Set β} [Preorder α] (hs : Pairwise (Function.onFun Disjoint s)) {i j : α} (hij : i < j) : Disjoint (accumulate s i) (s j)

@[simp]

theorem Set.accumulate_succ {α : Type u_1} (u : ℕ → Set α) (n : ℕ) : accumulate u (n + 1) = accumulate u n ∪ u (n + 1)

theorem Set.partialSups_eq_accumulate {α : Type u_1} (f : ℕ → Set α) : ⇑(partialSups f) = accumulate f

theorem Set.exists_subset_accumulate_of_directed {α : Type u_1} {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) (n : ℕ) : ∃ (m : ℕ), accumulate s n ⊆ s m

For a directed set of sets s : ℕ → Set α and n : ℕ, there exists m : ℕ (maybe larger than n) such that accumulate s n ⊆ s m.

theorem Set.directed_accumulate {α : Type u_1} {s : ℕ → Set α} : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) (accumulate s)

theorem Set.exists_accumulate_eq_univ_iff_of_directed {α : Type u_1} {s : ℕ → Set α} (hd : Directed (fun (x1 x2 : Set α) => x1 ⊆ x2) s) : (∃ (n : ℕ), accumulate s n = univ) ↔ ∃ (n : ℕ), s n = univ