Accumulate #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
theorem
set.subset_accumulate
{α : Type u_1}
{β : Type u_2}
{s : α → set β}
[preorder α]
{x : α} :
s x ⊆ set.accumulate s x