mathlib documentation

data.set.accumulate

Accumulate #

The function accumulate takes a set s and returns ⋃ y ≤ x, s y.

def set.accumulate {α : Type u_1} {β : Type u_2} [has_le α] (s : α → set β) (x : α) :
set β

accumulate s is the union of s y for y ≤ x.

Equations
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 : α} :
theorem set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : α → set β} [preorder α] :
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