mathlib3 documentation

data.set.accumulate

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.

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