Documentation

Mathlib.Data.Set.Accumulate

Accumulate #

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

def Set.Accumulate {α : Type u_1} {β : Type u_2} [inst : LE α] (s : αSet β) (x : α) :
Set β

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

Equations
theorem Set.accumulate_def {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : LE α] {x : α} :
Set.Accumulate s x = Set.unionᵢ fun y => Set.unionᵢ fun h => s y
@[simp]
theorem Set.mem_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : LE α] {x : α} {z : β} :
z Set.Accumulate s x y, y x z s y
theorem Set.subset_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : Preorder α] {x : α} :
theorem Set.monotone_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : Preorder α] :
theorem Set.bunionᵢ_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : Preorder α] (x : α) :
(Set.unionᵢ fun y => Set.unionᵢ fun h => Set.Accumulate s y) = Set.unionᵢ fun y => Set.unionᵢ fun h => s y
theorem Set.unionᵢ_accumulate {α : Type u_1} {β : Type u_2} {s : αSet β} [inst : Preorder α] :
(Set.unionᵢ fun x => Set.Accumulate s x) = Set.unionᵢ fun x => s x