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 ℕ.
accumulate s is the union of s y for y ≤ x.
Instances For
@[deprecated Set.accumulate (since := "2025-12-14")]
Alias of Set.accumulate.
accumulate s is the union of s y for y ≤ x.
Instances For
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.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