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 : α) (H : y ≤ x), s y
theorem
set.accumulate_def
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[has_le α]
{x : α} :
set.accumulate s x = ⋃ (y : α) (H : y ≤ x), s y
@[simp]
theorem
set.mem_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[has_le α]
{x : α}
{z : β} :
z ∈ set.accumulate s x ↔ ∃ (y : α) (H : y ≤ x), z ∈ s y
theorem
set.subset_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[preorder α]
{x : α} :
s x ⊆ set.accumulate s x
theorem
set.bUnion_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[preorder α]
(x : α) :
(⋃ (y : α) (H : y ≤ x), set.accumulate s y) = ⋃ (y : α) (H : y ≤ x), s y
theorem
set.Union_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[preorder α] :
(⋃ (x : α), set.accumulate s x) = ⋃ (x : α), s x