Accumulate #
The function Accumulate takes a set s and returns ⋃ y ≤ x, s y.
Accumulate s is the union of s y for y ≤ x.
Equations
- Set.Accumulate s x = ⋃ (y : α), ⋃ (_ : y ≤ x), s y
Instances For
theorem
Set.accumulate_def
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[LE α]
{x : α}
:
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 ∈ 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 β}
[Preorder α]
(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
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
theorem
Set.iUnion_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[Preorder α]
:
⋃ (x : α), Accumulate s x = ⋃ (x : α), s x