Accumulate #
The function Accumulate takes a set s and returns ⋃ y ≤ x, s y⋃ y ≤ x, s y≤ x, s y.
Accumulate s is the union of s y for y ≤ x≤ x.
Equations
- Set.Accumulate s x = Set.unionᵢ fun y => Set.unionᵢ fun h => s y
theorem
Set.accumulate_def
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[inst : LE α]
{x : α}
:
Set.Accumulate s x = Set.unionᵢ fun y => Set.unionᵢ fun h => s y
theorem
Set.subset_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[inst : Preorder α]
{x : α}
:
s x ⊆ Set.Accumulate s x
theorem
Set.bunionᵢ_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[inst : Preorder α]
(x : α)
:
(Set.unionᵢ fun y => Set.unionᵢ fun h => Set.Accumulate s y) = Set.unionᵢ fun y => Set.unionᵢ fun h => s y
theorem
Set.unionᵢ_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → Set β}
[inst : Preorder α]
:
(Set.unionᵢ fun x => Set.Accumulate s x) = Set.unionᵢ fun x => s x