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